(X Y : pType) : loops (X * Y) <~>* loops X * loops Y. Proof. snrapply Build_pEquiv'. 1: exact (equiv_path_prod (point (X * Y)) (point (X * Y)))^-1%equiv. reflexivity. 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.