`{Funext} (P : Type) : {b : P & b = b} <~> (Circle -> P) := Build_Equiv _ _ _ (isequiv_Circle_rec_uncurried P).
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.