`{Funext} {A B C} (f : A -> B) (g : A -> C) P : {psh : (B -> P) * (C -> P) & forall a, fst psh (f a) = snd psh (g a) } <~> (Pushout f g -> P) := Build_Equiv _ _ _ (isequiv_Pushout_rec f g P).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.