fact: Definition Trunc_functor_idmap (X : Type) : @Trunc_functor X X idmap == idmap := O_functor_idmap (Tr n) X.
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality