sig pushout_flatten_fam <~> Pushout (functor_sigma f (fun _ => idmap)) (functor_sigma g e). Proof. unfold pushout_flatten_fam. refine (_ oE equiv_coeq_flatten _ _). unfold Pushout. snrapply equiv_functor_coeq'. - reflexivity. - apply equiv_sigma_sum. - reflexivity. - reflexivity. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.