fact: Definition Circle_code : Circle -> Type := Circle_rec Type Int (path_universe int_succ).
imports: Basics Types Pointed.Core Pointed.Loops Pointed.pEquiv HSet Spaces.Pos Spaces.Int Colimits.Coeq Truncations.Core Truncations.Connectedness Cubical.DPath