fact: Definition functor_susp_compose {X Y Z} (f : X -> Y) (g : Y -> Z) : functor_susp (g o f) == functor_susp g o functor_susp f.
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions