proposition: Lemma iterated_loops_prod (X Y : pType) {n} : iterated_loops n (X * Y) <~>* (iterated_loops n X) * (iterated_loops n Y).
proof: Proof. induction n as [|n IHn]. 1: reflexivity. exact (loops_prod _ _ o*E emap loops IHn). Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core