fact: Definition pequiv_ptr_rec `{Funext} {n} {X Y : pType} `{IsTrunc n Y} : (pTr n X ->** Y) <~>* (X ->** Y) := pequiv_o_pto_O _ X Y.
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality