`{Funext} {A B C} (f : A -> B) (g : A -> C) P : IsEquiv (fun p : {psh : (B -> P) * (C -> P) & forall a, fst psh (f a) = snd psh (g a) } => Pushout_rec P (fst p.1) (snd p.1) p.2). Proof. srefine (isequiv_adjointify _ (pushout_unrec f g) _ _). - intro e. apply path_arrow. apply pushout_rec_unrec. - intros [[pushb pushc] pusha]; unfold pushout_unrec; cbn. snrapply path_sigma'. + reflexivity. + cbn. apply path_forall; intros a. apply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.