(base = base) <~> Int := Build_Equiv _ _ (Circle_encode base) (Circle_encode_isequiv base). End EncodeDecode. Global Instance isconnected_Circle `{Univalence} : IsConnected 0 Circle. Proof. apply is0connected_merely_allpath. 1: exact (tr base). srefine (Circle_ind _ _ _). - simple refine (Circle_ind _ _ _). + exact (tr 1). + apply path_ishprop. - apply path_ishprop. 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.