fact: Definition ptr_natural_path (n : trunc_index) {X Y : pType} (f : X ->* Y) : fmap (pTr n) f o* ptr = ptr o* f := pTr_rec_beta_path n (ptr o* f).
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality