Pushout f g <~> Pushout f' g'. 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.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.