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