{B A f g} {P : @Coeq B A f g -> Type} (h : forall w : Coeq f g, P w) : h == Coeq_ind P (h o coeq) (fun b => apD h (cglue b)). Proof. unfold pointwise_paths. nrapply (Coeq_ind _ (fun _ => 1)). intros b. lhs nrapply transport_paths_FlFr_D. lhs nrapply (whiskerL _ (Coeq_ind_beta_cglue _ _ _ _)). lhs nrapply (whiskerR (concat_p1 _)). nrapply concat_Vp. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.