fact: Definition Trunc_rec_tr n {A : Type} : Trunc_rec (A:=A) (tr (n:=n)) == idmap := Trunc_ind _ (fun a => idpath).
imports: Basics Types WildCat.Core WildCat.Universe Modalities.Modality (coercions) Modalities.Modality