{A B C P} (f : A -> B) (g : A -> C) (h : Pushout f g -> P) : {psh : (B -> P) * (C -> P) & forall a, fst psh (f a) = snd psh (g a)}. Proof. exists (h o pushl, h o pushr). intros a; cbn. exact (ap h (pglue a)). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.