forall x y, P x y. Proof. simple refine (Coeq_ind _ _ _). - intros a. simple refine (Coeq_ind _ _ _). + intros a'. exact (coeq' a a'). + intros b'; cbn. apply cgluer. - intros b. apply path_forall; intros a. revert a; simple refine (Coeq_ind _ _ _). + intros a'. cbn. refine (transport_forall_constant _ _ _ @ _). apply cgluel. + intros b'; cbn. refine (transport_paths_FlFr_D (cglue b') _ @ _). rewrite Coeq_ind_beta_cglue. Open Scope long_path_scope. rewrite ap_pp. repeat rewrite concat_p_pp. set (G := (Coeq_ind (P (coeq (f b))) (fun a' : A' => coeq' (f b) a') (fun b'0 : B' => cgluer (f b) b'0))). rewrite (apD_transport_forall_constant P (cglue b) G (cglue b')); simpl. rewrite !inv_pp, !inv_V. rewrite !concat_pp_p; apply whiskerL. rewrite !concat_p_pp, concat_pV_p. subst G; rewrite Coeq_ind_beta_cglue; simpl. rewrite !concat_pp_p; do 2 apply moveR_Vp; rewrite !concat_p_pp. apply cgluelr. 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.