fact: Definition pushout_sym_map {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)^).
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq