{A B A' B'} (f : A -> A') (g : B -> B') (P : A' + B' -> Type) (ef : ExtendableAlong 1 f (P o inl)) (eg : ExtendableAlong 1 g (P o inr)) (h : forall z, P (functor_sum f g z)) : ExtensionAlong (functor_sum f g) P h. Proof. srefine (sum_ind _ _ _ ; sum_ind _ _ _). + exact (fst ef (h o inl)).1. + exact (fst eg (h o inr)).1. + exact (fst ef (h o inl)).2. + exact (fst eg (h o inr)).2. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.