`{Funext} (X : pType) : (pCircle ->** X) <~>* loops X. Proof. snrapply Build_pEquiv'. - refine (_ oE (issig_pmap _ _)^-1%equiv). equiv_via { xp : { x : X & x = x } & xp.1 = pt }. 2: make_equiv_contr_basedpaths. exact ((equiv_functor_sigma_pb (equiv_Circle_rec X)^-1%equiv)). - simpl. apply ap_const. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.Loops Pointed.pEquiv. Require Import HSet. Require Import Spaces.Int. Require Import Colimits.Coeq. Require Import Truncations.Core Truncations.Connectedness.