{X Y : Type} (f : X -> Y) (P : Susp Y -> Type) (n : nat) : (ExtendableAlong n (functor_susp f) P) <-> (forall NS, ExtendableAlong n f (fun x => DPath P (merid x) (fst NS) (snd NS))). Proof. revert P. induction n as [|n IHn]; intros P; [ split; intros; exact tt | ]. split. - intros [e1 en] [N S]; split. + apply extension_iff_functor_susp. exact e1. + cbn; intros h k. pose (h' := Susp_ind P N S h). pose (k' := Susp_ind P N S k). specialize (en h' k'). assert (IH := fst (IHn _) en (1,1)); clear IHn en. cbn in IH. refine (extendable_postcompose' n _ _ f _ IH); clear IH. intros y. etransitivity. 1: nrapply ds_dp. etransitivity. 1: apply ds_transport_dpath. subst h' k'; cbn. apply equiv_concat_lr. * symmetry. exact (Susp_ind_beta_merid P N S h y). * exact (Susp_ind_beta_merid P N S k y). - intros e; split. + apply extension_iff_functor_susp. intros NS; exact (fst (e NS)). + intros h k. apply (IHn _). intros [p q]. specialize (e (h North, k South)). cbn in *; apply snd in e. refine (extendable_postcompose' n _ _ f _ (e _ _)); intros y. symmetry. etransitivity. 1: nrapply ds_dp. etransitivity. 1: apply ds_transport_dpath. etransitivity. 1: reflexivity. symmetry. apply (equiv_moveR_transport_p (fun y0 : P North => DPath P (merid y) y0 (k South))). 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.