{B A f g B' A' f' g'} (h : B -> B') (k : A -> A') (p : k o f == f' o h) (q : k o g == g' o h) (h' : B -> B') (k' : A -> A') (p' : k' o f == f' o h') (q' : k' o g == g' o h') (r : h == h') (s : k == k') (u : forall b, s (f b) @ p' b = p b @ ap f' (r b)) (v : forall b, s (g b) @ q' b = q b @ ap g' (r b)) : functor_coeq h k p q == functor_coeq h' k' p' q'. Proof. refine (Coeq_ind _ (fun a => ap coeq (s a)) _); cbn; intros b. refine (transport_paths_FlFr (cglue b) _ @ _). rewrite concat_pp_p; apply moveR_Vp. rewrite !functor_coeq_beta_cglue. Open Scope long_path_scope. rewrite !concat_p_pp. rewrite <- (ap_pp (@coeq _ _ f' g') (s (f b)) (p' b)). rewrite u, ap_pp, !concat_pp_p; apply whiskerL; rewrite !concat_p_pp. rewrite ap_V; apply moveR_pV. rewrite !concat_pp_p, <- (ap_pp (@coeq _ _ f' g') (s (g b)) (q' b)). rewrite v, ap_pp, ap_V, concat_V_pp. rewrite <- !ap_compose. exact (concat_Ap (@cglue _ _ f' g') (r b)). Close Scope long_path_scope. Qed.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.