fact: Definition pequiv_ptr_functor {X Y : pType} (n : trunc_index) (f : X <~>* Y) : pTr n X <~>* pTr n Y := emap (pTr n) f.
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality