{A B C : Type} {f : A -> B} {g : A -> C} {A' B' C' : Type} {f' : A' -> B'} {g' : A' -> C'} {h h' : A -> A'} {k k' : B -> B'} {l l' : C -> C'} {p : k o f == f' o h} {q : l o g == g' o h} {p' : k' o f == f' o h'} {q' : l' o g == g' o h'} (t : h == h') (u : k == k') (v : l == l') (i : forall a, p a @ (ap f') (t a) = u (f a) @ p' a) (j : forall a, q a @ (ap g') (t a) = v (g a) @ q' a) : functor_pushout h k l p q == functor_pushout h' k' l' p' q'. Proof. srapply functor_coeq_homotopy. 1: exact t. 1: exact (functor_sum_homotopic u v). 1,2: intros b; simpl. 1,2: refine (_ @ ap_pp _ _ _ @ ap _ (ap_compose _ _ _)^). 1,2: refine ((ap_pp _ _ _)^ @ ap _ _^). 1: exact (i b). exact (j b). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.