(x : Circle) : Circle_code x -> (base = x). Proof. revert x; refine (Circle_ind (fun x => Circle_code x -> base = x) (loopexp loop) _). apply path_forall; intros z; simpl in z. refine (transport_arrow _ _ _ @ _). refine (transport_paths_r loop _ @ _). rewrite transport_Circle_code_loopV. rewrite loopexp_pred_r. apply concat_pV_p. 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.