proposition: Lemma loops_prod (X Y : pType) : loops (X * Y) <~>* loops X * loops Y.
proof: Proof. snrapply Build_pEquiv'. 1: exact (equiv_path_prod (point (X * Y)) (point (X * Y)))^-1%equiv. reflexivity. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core