fact: Definition isequiv_Trunc_functor {X Y} (f : X -> Y) `{IsEquiv _ _ f} : IsEquiv (Trunc_functor f) := isequiv_O_functor (Tr n) f.
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality