(A : pType) : loops A <~>* loops A. Proof. srapply Build_pEquiv. 1: exact (Build_pMap (loops A) (loops A) inverse 1). apply isequiv_path_inverse. 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.