fact: Definition pequiv_pi_Tr `{Univalence} (n : nat) (X : pType) : Pi n X <~>* Pi n (pTr n X) := Build_pEquiv _ _ (fmap (pPi n) ptr) _.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat