n {A} {P Q : A -> Type} (f : forall a, P a -> Q a) (C : sig Q -> Type) (ef : forall a, ExtendableAlong n (f a) (fun v => C (a;v))) : ExtendableAlong n (functor_sigma idmap f) C. Proof. revert C ef; simple_induction n n IH; intros C ef; [ exact tt | split ]. - apply extension_functor_sigma_id. intros a; exact (fst (ef a) , fun _ _ => tt). - intros h k; apply IH. intros a; apply (snd (ef a)). 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.