{A B C} {f : A -> B} {g : A -> C} {A' B' C'} {f' : A' -> B'} {g' : A' -> C'} (h : A -> A') (k : B -> B') (l : C -> C') (p : k o f == f' o h) (q : l o g == g' o h) : Pushout f g -> Pushout f' g'. Proof. unfold Pushout; srapply functor_coeq. - exact h. - exact (functor_sum k l). - intros a; cbn. apply ap, p. - intros a; cbn. apply ap, q. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.