(x:Circle) : IsEquiv (Circle_encode x). Proof. refine (isequiv_adjointify (Circle_encode x) (Circle_decode x) _ _). - refine (Circle_ind (fun x => (Circle_encode x) o (Circle_decode x) == idmap) Circle_encode_loopexp _ _). by apply path_forall; intros z; apply hset_path2. - intros []; reflexivity. 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.