fact: Definition equiv_sigma_pushout : { x : X & Pushout (f x) (g x) } <~> Pushout (functor_sigma idmap f) (functor_sigma idmap g).
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq