fact: Definition pTr_rec_beta n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y) : pTr_rec n f o* ptr ==* f := phomotopy_path (pTr_rec_beta_path n f).
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality