(n : nat) {A B A' B'} (f : A -> A') (g : B -> B') (P : A' + B' -> Type) (ef : ExtendableAlong n f (P o inl)) (eg : ExtendableAlong n g (P o inr)) : ExtendableAlong n (functor_sum f g) P. Proof. revert P ef eg; induction n as [|n IH]; intros P ef eg; [ exact tt | split ]. - intros h; apply extension_functor_sum. + exact (fst ef, fun _ _ => tt). + exact (fst eg, fun _ _ => tt). - intros h k. apply IH. + exact (snd ef (h o inl) (k o inl)). + exact (snd eg (h o inr) (k o inr)). 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.