fact: Definition trunc_iff_isequiv_truncation (A : Type) : IsTrunc n A <-> IsEquiv (@tr n A) := inO_iff_isequiv_to_O (Tr n) A.
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality