unfold_iterated_loops' (n : nat) (X : pType) : iterated_loops n.+1 X <~>* iterated_loops n (loops X). Proof. induction n. 1: reflexivity. change (iterated_loops n.+2 X) with (loops (iterated_loops n.+1 X)). apply pequiv_fmap_loops, IHn. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.