Coeq f g -> Coeq f' g' -> P. Proof. intros x y; revert x. snrapply Coeq_rec. - intros a. revert y. snrapply Coeq_rec. + intros a'. exact (coeq' a a'). + intros b'; cbn. apply cgluer. - intros b. revert y. snrapply Coeq_ind. + intros a'. cbn. apply cgluel. + intros b'. nrapply (transport_paths_FlFr' (cglue b')). lhs nrapply (_ @@ 1). 1: apply Coeq_rec_beta_cglue. rhs nrapply (1 @@ _). 2: apply Coeq_rec_beta_cglue. symmetry. apply cgluelr. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.