`{Funext} {n} {X Y : pType} `{IsTrunc n Y} : (pTr n X ->** Y) <~>* (X ->** Y) := pequiv_o_pto_O _ X Y. Global Instance is0functor_ptr n : Is0Functor (pTr n). Proof. apply Build_Is0Functor. intros X Y f. exact (pTr_rec _ (ptr o* f)). Defined.
Require Import Basics Types WildCat Truncations