fact: Definition pequiv_ptr {n : trunc_index} {A : pType} `{IsTrunc n A} : A <~>* pTr n A := @pequiv_pto (Tr n) A _.
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality