{A B} {P : A -> Type} {Q : B -> Type} (f : A -> B) (g : forall a, P a -> Q (f a)) (C : sig Q -> Type) (ef : ooHomotopyExtendableAlong f C) (eg : forall a, ooExtendableAlong (g a) (fun v => C (f a ; v))) : ooExtendableAlong (functor_sigma f g) C := fun n => extendable_functor_sigma n f g C (ef n) (fun a => eg a n).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.