fact: Definition iterated_loops (n : nat) (A : pType) : pType := nat_iter n loops A.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core