{A B A' B'} (f : A -> A') (g : B -> B') (P : A' + B' -> Type) (ef : ooExtendableAlong f (P o inl)) (eg : ooExtendableAlong g (P o inr)) : ooExtendableAlong (functor_sum f g) P. Proof. intros n; apply extendable_functor_sum; [ apply ef | apply eg ]. 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.