fact: Definition equiv_pushout_flatten : sig pushout_flatten_fam <~> Pushout (functor_sigma f (fun _ => idmap)) (functor_sigma g e).
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq