proposition: Lemma iterated_loops_pproduct_commute `{Funext} (A : Type) (F : A -> pType) (n : nat) : iterated_loops n (pproduct F) <~>* pproduct (iterated_loops n o F).
proof: Proof. induction n. 1: reflexivity. refine (loops_pproduct_commute _ _ o*E _). rapply (emap loops). exact IHn. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core