`{Funext} {B A} (f g : B -> A) P : IsEquiv (fun p : {h : A -> P & h o f == h o g} => Coeq_rec P p.1 p.2). Proof. srapply (isequiv_adjointify _ (Coeq_unrec f g)). - intros h. apply path_arrow. srapply Coeq_ind; intros b. 1: cbn;reflexivity. cbn. nrapply transport_paths_FlFr'. apply equiv_p1_1q. nrapply Coeq_rec_beta_cglue. - intros [h q]; srapply path_sigma'. + reflexivity. + cbn. rapply path_forall; intros b. apply Coeq_rec_beta_cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.