{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' o h == idmap) (s : k' o k == idmap) (u : forall b, ap k' (p b) @ p' (h b) @ ap f (r b) = s (f b)) (v : forall b, ap k' (q b) @ q' (h b) @ ap g (r b) = s (g b)) : (functor_coeq h' k' p' q') o (functor_coeq h k p q) == idmap. Proof. refine (Coeq_ind _ (fun a => ap coeq (s a)) _); cbn; intros b. refine (transport_paths_FFlr (cglue b) _ @ _). rewrite concat_pp_p; apply moveR_Vp. rewrite functor_coeq_beta_cglue, !ap_pp. rewrite <- !ap_compose; cbn. rewrite functor_coeq_beta_cglue. Open Scope long_path_scope. rewrite !concat_p_pp. rewrite <- u, !ap_pp, !(ap_compose k' coeq). rewrite !concat_pp_p; do 2 apply whiskerL. rewrite !concat_p_pp. rewrite <- v. rewrite !ap_pp, !ap_V, !concat_p_pp, !concat_pV_p. rewrite <- !ap_compose. exact (concat_Ap cglue (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.