`{Funext} (A : Type) (F : A -> pType) : loops (pproduct F) <~>* pproduct (loops o F). Proof. snrapply Build_pEquiv'. 1: apply equiv_apD10. 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.