(n : nat) {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 n f C) (eg : forall a, ExtendableAlong n (g a) (fun v => C (f a ; v))) : ExtendableAlong n (functor_sigma f g) C. Proof. revert C ef eg; simple_induction n n IH; intros C ef eg; [ exact tt | split ]. - apply extension_functor_sigma. + exact (fst ef, fun _ _ => tt). + intros a; exact (fst (eg a) , fun _ _ => tt). - intros h k; apply IH. + exact (snd ef h k). + intros a; apply (snd (eg 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.