fact: Definition functor_Susp_ind_type : Susp_ind_type Y P -> Susp_ind_type X (P o functor_susp f) := fun g => g o functor_susp f.
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions