fact: Definition equiv_path_Tr `{Univalence} {n} {A : Type} (x y : A) : Tr n (x = y) <~> (tr x = tr y :> Tr n.+1 A) := equiv_path_OO (Tr n.+1) (Tr n) x y.
imports: Basics Types TruncType Truncations.Core Modalities.Modality Modalities.Descent