(P : Type) : {b : P & b = b} -> (Circle -> P) := fun x => Circle_rec P (pr1 x) (pr2 x). Global Instance isequiv_Circle_rec_uncurried `{Funext} (P : Type) : IsEquiv ( P). Proof. srapply isequiv_adjointify. - exact (fun g => (g base ; ap g loop)). - intros g. apply path_arrow. srapply Circle_ind. + reflexivity. + unfold ; cbn. apply transport_paths_FlFr'. apply equiv_p1_1q. apply Circle_rec_beta_loop. - intros [b p]; apply ap. apply Circle_rec_beta_loop. 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.