proposition: Lemma loops_pproduct_commute `{Funext} (A : Type) (F : A -> pType) : loops (pproduct F) <~>* pproduct (loops o F).
proof: Proof. snrapply Build_pEquiv'. 1: apply equiv_apD10. reflexivity. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core