{B A f g} (P : @Coeq B A f g -> Type) {m n : forall a, P (coeq a)} (u : m == n) {r : forall b, (cglue b) # (m (f b)) = m (g b)} {s : forall b, (cglue b) # (n (f b)) = n (g b)} (p : forall b, ap (transport P (cglue b)) (u (f b)) @ (s b) = r b @ u (g b)) : Coeq_ind P m r == Coeq_ind P n s. Proof. unfold pointwise_paths. nrapply Coeq_ind; intros b. lhs nrapply (transport_paths_FlFr_D (f:=Coeq_ind P m r) (g:=Coeq_ind P n s)). lhs nrapply (whiskerL _ (Coeq_ind_beta_cglue P n s b)). lhs nrapply (whiskerR (whiskerR (ap inverse (Coeq_ind_beta_cglue P m r b)) _)). lhs nrapply concat_pp_p; nrapply moveR_Mp. rhs nrapply (whiskerR (inv_V _)). exact (p b). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.