{B A f g} {P : Type} (h : @Coeq B A f g -> P) : h == Coeq_rec P (h o coeq) (fun b => ap h (cglue b)). Proof. unfold pointwise_paths. nrapply (Coeq_ind _ (fun _ => 1)). intros b. apply transport_paths_FlFr', equiv_p1_1q. symmetry; nrapply Coeq_rec_beta_cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.