proposition: Lemma local_global_looping `{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: 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.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core