fact: Definition ptr_loops_eq `{Univalence} (n : trunc_index) (A : pType) : pTr n (loops A) = loops (pTr n.+1 A) :> pType := path_ptype (ptr_loops n A).
imports: Basics Types WildCat Truncations Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality