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