(forall g, ExtensionAlong (functor_susp f) P g) <-> (forall NS g, ExtensionAlong f (fun x => DPath P (merid x) (fst NS) (snd NS)) g). Proof. transitivity (SplEssSurj functor_Susp_ind_type). { reflexivity. } etransitivity. { refine (isesssurj_iff_commsq Susp_ind_inv_nat); try exact _. all:apply issurjinj_Susp_ind_inv. } etransitivity. { refine (isesssurj_iff_sigma _ _ (fun NS => functor_Susp_ind_data' NS o functor_Susp_ind_data'' NS)). } apply iff_functor_forall; intros [N S]; cbn. etransitivity. { apply iffL_isesssurj; exact _. } reflexivity. 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.