proposition: Lemma equiv_pushout : Pushout f g <~> Pushout f' g'.
proof: Proof. refine (equiv_functor_coeq' eA (equiv_functor_sum' eB eC) _ _). all:unfold pointwise_paths. all:intro; simpl; apply ap. + apply p. + apply q. Defined.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq