{A B C} {f : A -> B} {g : A -> C} : Pushout f g -> Pushout g f := Pushout_rec (Pushout g f) pushr pushl (fun a : A => (pglue a)^).
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.