(X Y : pType) {n} : iterated_loops n (X * Y) <~>* (iterated_loops n X) * (iterated_loops n Y). Proof. induction n as [|n IHn]. 1: reflexivity. exact (loops_prod _ _ o*E emap 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.