{A B} {P : A -> Type} {Q : B -> Type} (f : A -> B) (g : forall a, P a -> Q (f a)) (C : sig Q -> Type) (ef : HomotopyExtendableAlong 1 f C) (eg : forall a, ExtendableAlong 1 (g a) (fun v => C (f a ; v))) (s : forall z, C (functor_sigma f g z)) : ExtensionAlong (functor_sigma f g) C s. Proof. srefine (_;_). - intros [b v]; revert b v. refine ((fst ef _).1). intros a. refine ((fst (eg a) _).1). intros u. exact (s (a;u)). - intros [a u]; cbn. refine ((fst ef _).2 _ _ @ _). exact ((fst (eg a) _).2 u). 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.