`{Univalence} (A : Type@{i}) (n : nat) : iterated_loops@{j} n.+2 [Type@{i}, A] <~>* pproduct (fun a => iterated_loops@{j} n.+1 [A, a]). Proof. induction n. { refine (_ o*E emap loops (loops_type A)). apply issig_pequiv'. exists (equiv_inverse (equiv_path_arrow 1%equiv 1%equiv) oE equiv_inverse (equiv_path_equiv 1%equiv 1%equiv)). reflexivity. } exact (loops_pproduct_commute _ _ 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.