n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y) : pTr_rec n f o* ptr = f. Proof. unfold pTr_rec, "o*"; cbn. apply (ap (Build_pMap _ _ f)). apply concat_1p. Defined.
Require Import Basics Types WildCat Truncations