`{Funext} {A : pType} (B : A -> pType) : loops (ppforall x : A, B x) <~>* (ppforall x : A, loops (B x)). Proof. srapply Build_pEquiv'. 1: symmetry; exact (equiv_path_pforall (point_pforall B) (point_pforall B)). 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.