fact: Definition unfold_iterated_loops (n : nat) (X : pType) : iterated_loops n.+1 X = iterated_loops n (loops X) := nat_iter_succ_r _ _ _.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core