{A B C} {f : A -> B} {g : A -> C} : Pushout f g <~> Pushout g f := equiv_adjointify pushout_sym_map pushout_sym_map sect_pushout_sym_map sect_pushout_sym_map.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.