{X Y : Type} (f : X -> Y) (P : Susp Y -> Type) : (ooExtendableAlong (functor_susp f) P) <-> (forall NS, ooExtendableAlong f (fun x => DPath P (merid x) (fst NS) (snd NS))). Proof. split; intros e. - intros NS n. apply extendable_iff_functor_susp. exact (e n). - intros n. apply extendable_iff_functor_susp. intros NS; exact (e NS n). Defined.
Require Import Basics. Require Import Types. Require Import Cubical.DPath Cubical.DPathSquare. Require Import WildCat. Require Import Colimits.Pushout. Require Import NullHomotopy. Require Import Truncations.Core. Require Import Modalities.Modality. Require Import Extensions.