{B A f g 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') : functor_coeq (h' o h) (k' o k) (fun b => ap k' (p b) @ p' (h b)) (fun b => ap k' (q b) @ q' (h b)) == functor_coeq h' k' p' q' o functor_coeq h k p q. Proof. refine (Coeq_ind _ (fun a => 1) _); cbn; intros b. nrapply transport_paths_FlFr'. apply equiv_p1_1q; symmetry. rewrite ap_compose. rewrite !functor_coeq_beta_cglue, !ap_pp, functor_coeq_beta_cglue. rewrite <- !ap_compose. cbn. rewrite !ap_V, ap_pp, inv_pp, <- ap_compose, !concat_p_pp. reflexivity. Qed.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.