fact: Definition functor_Susp_ind_data' (NS : P North * P South) : Susp_ind_data'' NS -> Susp_ind_data' X (P o functor_susp f) NS.
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions