Cyclic types

module univalent-combinatorics.cyclic-types where
Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.groups-of-modular-arithmetic
open import elementary-number-theory.integers
open import elementary-number-theory.modular-arithmetic
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers

open import foundation.0-connected-types
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.mere-equality
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.groups
open import group-theory.isomorphisms-groups

open import higher-group-theory.higher-groups

open import structured-types.equivalences-types-equipped-with-endomorphisms
open import structured-types.mere-equivalences-types-equipped-with-endomorphisms
open import structured-types.pointed-types
open import structured-types.types-equipped-with-endomorphisms

open import synthetic-homotopy-theory.groups-of-loops-in-1-types
open import synthetic-homotopy-theory.loop-spaces

Idea

A cyclic type is a type X equipped with an endomorphism f : X → X such that the pair (X, f) is merely equivalent to the pair (ℤ-Mod k, +1) for some k : ℕ.

Definitions

The type of cyclic types of a given order

is-cyclic-Endo : {l : Level}    Endo l  UU l
is-cyclic-Endo k X = mere-equiv-Endo (ℤ-Mod-Endo k) X

Cyclic-Type : (l : Level)    UU (lsuc l)
Cyclic-Type l k = Σ (Endo l) (is-cyclic-Endo k)

module _
  {l : Level} (k : ) (X : Cyclic-Type l k)
  where

  endo-Cyclic-Type : Endo l
  endo-Cyclic-Type = pr1 X

  type-Cyclic-Type : UU l
  type-Cyclic-Type = type-Endo endo-Cyclic-Type

  endomorphism-Cyclic-Type : type-Cyclic-Type  type-Cyclic-Type
  endomorphism-Cyclic-Type = endomorphism-Endo endo-Cyclic-Type

  mere-equiv-endo-Cyclic-Type : mere-equiv-Endo (ℤ-Mod-Endo k) endo-Cyclic-Type
  mere-equiv-endo-Cyclic-Type = pr2 X

  is-set-type-Cyclic-Type : is-set type-Cyclic-Type
  is-set-type-Cyclic-Type =
    apply-universal-property-trunc-Prop
      ( mere-equiv-endo-Cyclic-Type)
      ( is-set-Prop type-Cyclic-Type)
      ( λ e 
        is-set-equiv'
          ( ℤ-Mod k)
          ( equiv-equiv-Endo (ℤ-Mod-Endo k) endo-Cyclic-Type e)
          ( is-set-ℤ-Mod k))

  set-Cyclic-Type : Set l
  pr1 set-Cyclic-Type = type-Cyclic-Type
  pr2 set-Cyclic-Type = is-set-type-Cyclic-Type

Cyclic-Type structure on a type

cyclic-structure : {l : Level}    UU l  UU l
cyclic-structure k X = Σ (X  X)  f  is-cyclic-Endo k (pair X f))

cyclic-type-cyclic-structure :
  {l : Level} (k : ) {X : UU l}  cyclic-structure k X  Cyclic-Type l k
pr1 (pr1 (cyclic-type-cyclic-structure k {X} c)) = X
pr2 (pr1 (cyclic-type-cyclic-structure k c)) = pr1 c
pr2 (cyclic-type-cyclic-structure k c) = pr2 c

The standard cyclic types

ℤ-Mod-Cyclic-Type : (k : )  Cyclic-Type lzero k
pr1 (ℤ-Mod-Cyclic-Type k) = ℤ-Mod-Endo k
pr2 (ℤ-Mod-Cyclic-Type k) = refl-mere-equiv-Endo (ℤ-Mod-Endo k)

Fin-Cyclic-Type : (k : )  Cyclic-Type lzero (succ-ℕ k)
Fin-Cyclic-Type k = ℤ-Mod-Cyclic-Type (succ-ℕ k)

Cyclic-Type-Pointed-Type : (k : )  Pointed-Type (lsuc lzero)
pr1 (Cyclic-Type-Pointed-Type k) = Cyclic-Type lzero k
pr2 (Cyclic-Type-Pointed-Type k) = ℤ-Mod-Cyclic-Type k

Equivalences of cyclic types

module _
  {l1 l2 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k)
  where

  equiv-Cyclic-Type : UU (l1  l2)
  equiv-Cyclic-Type = equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y)

  equiv-equiv-Cyclic-Type :
    equiv-Cyclic-Type  type-Cyclic-Type k X  type-Cyclic-Type k Y
  equiv-equiv-Cyclic-Type =
    equiv-equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y)

  map-equiv-Cyclic-Type :
    equiv-Cyclic-Type  type-Cyclic-Type k X  type-Cyclic-Type k Y
  map-equiv-Cyclic-Type e =
    map-equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y) e

  coherence-square-equiv-Cyclic-Type :
    (e : equiv-Cyclic-Type) 
    coherence-square-maps
      ( map-equiv-Cyclic-Type e)
      ( endomorphism-Cyclic-Type k X)
      ( endomorphism-Cyclic-Type k Y)
      ( map-equiv-Cyclic-Type e)
  coherence-square-equiv-Cyclic-Type e = pr2 e

module _
  {l : Level} (k : ) (X : Cyclic-Type l k)
  where

  id-equiv-Cyclic-Type : equiv-Cyclic-Type k X X
  id-equiv-Cyclic-Type = id-equiv-Endo (endo-Cyclic-Type k X)

  equiv-eq-Cyclic-Type :
    (Y : Cyclic-Type l k)  Id X Y  equiv-Cyclic-Type k X Y
  equiv-eq-Cyclic-Type .X refl = id-equiv-Cyclic-Type

is-contr-total-equiv-Cyclic-Type :
  {l1 : Level} (k : ) (X : Cyclic-Type l1 k) 
  is-contr (Σ (Cyclic-Type l1 k) (equiv-Cyclic-Type k X))
is-contr-total-equiv-Cyclic-Type k X =
  is-contr-total-Eq-subtype
    ( is-contr-total-equiv-Endo (endo-Cyclic-Type k X))
    ( λ Y  is-prop-type-trunc-Prop)
    ( endo-Cyclic-Type k X)
    ( id-equiv-Endo (endo-Cyclic-Type k X))
    ( mere-equiv-endo-Cyclic-Type k X)

module _
  {l : Level} (k : ) (X : Cyclic-Type l k)
  where

  is-equiv-equiv-eq-Cyclic-Type :
    (Y : Cyclic-Type l k)  is-equiv (equiv-eq-Cyclic-Type k X Y)
  is-equiv-equiv-eq-Cyclic-Type =
    fundamental-theorem-id
      ( is-contr-total-equiv-Cyclic-Type k X)
      ( equiv-eq-Cyclic-Type k X)

  extensionality-Cyclic-Type :
    (Y : Cyclic-Type l k)  Id X Y  equiv-Cyclic-Type k X Y
  pr1 (extensionality-Cyclic-Type Y) = equiv-eq-Cyclic-Type k X Y
  pr2 (extensionality-Cyclic-Type Y) = is-equiv-equiv-eq-Cyclic-Type Y

  eq-equiv-Cyclic-Type :
    (Y : Cyclic-Type l k)  equiv-Cyclic-Type k X Y  Id X Y
  eq-equiv-Cyclic-Type Y = map-inv-is-equiv (is-equiv-equiv-eq-Cyclic-Type Y)

Properties

module _
  {l1 l2 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k)
  where

  htpy-equiv-Cyclic-Type : (e f : equiv-Cyclic-Type k X Y)  UU (l1  l2)
  htpy-equiv-Cyclic-Type e f =
    map-equiv-Cyclic-Type k X Y e ~ map-equiv-Cyclic-Type k X Y f

  refl-htpy-equiv-Cyclic-Type :
    (e : equiv-Cyclic-Type k X Y)  htpy-equiv-Cyclic-Type e e
  refl-htpy-equiv-Cyclic-Type e = refl-htpy

  htpy-eq-equiv-Cyclic-Type :
    (e f : equiv-Cyclic-Type k X Y)  Id e f  htpy-equiv-Cyclic-Type e f
  htpy-eq-equiv-Cyclic-Type e .e refl = refl-htpy-equiv-Cyclic-Type e

  is-contr-total-htpy-equiv-Cyclic-Type :
    (e : equiv-Cyclic-Type k X Y) 
    is-contr (Σ (equiv-Cyclic-Type k X Y) (htpy-equiv-Cyclic-Type e))
  is-contr-total-htpy-equiv-Cyclic-Type e =
    is-contr-equiv'
      ( Σ ( equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y))
          ( htpy-equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y) e))
      ( equiv-tot
        ( λ f 
          right-unit-law-Σ-is-contr
            ( λ H 
              is-contr-Π
                ( λ x 
                  is-set-type-Cyclic-Type k Y
                  ( map-equiv-Cyclic-Type k X Y e
                    ( endomorphism-Cyclic-Type k X x))
                  ( endomorphism-Cyclic-Type k Y
                    ( map-equiv-Cyclic-Type k X Y f x))
                  ( ( H (endomorphism-Cyclic-Type k X x)) 
                    ( coherence-square-equiv-Cyclic-Type k X Y f x))
                  ( ( coherence-square-equiv-Cyclic-Type k X Y e x) 
                    ( ap (endomorphism-Cyclic-Type k Y) (H x)))))))
      ( is-contr-total-htpy-equiv-Endo
        ( endo-Cyclic-Type k X)
        ( endo-Cyclic-Type k Y)
        ( e))

  is-equiv-htpy-eq-equiv-Cyclic-Type :
    (e f : equiv-Cyclic-Type k X Y)  is-equiv (htpy-eq-equiv-Cyclic-Type e f)
  is-equiv-htpy-eq-equiv-Cyclic-Type e =
    fundamental-theorem-id
      ( is-contr-total-htpy-equiv-Cyclic-Type e)
      ( htpy-eq-equiv-Cyclic-Type e)

  extensionality-equiv-Cyclic-Type :
    (e f : equiv-Cyclic-Type k X Y)  Id e f  htpy-equiv-Cyclic-Type e f
  pr1 (extensionality-equiv-Cyclic-Type e f) = htpy-eq-equiv-Cyclic-Type e f
  pr2 (extensionality-equiv-Cyclic-Type e f) =
    is-equiv-htpy-eq-equiv-Cyclic-Type e f

  eq-htpy-equiv-Cyclic-Type :
    (e f : equiv-Cyclic-Type k X Y)  htpy-equiv-Cyclic-Type e f  Id e f
  eq-htpy-equiv-Cyclic-Type e f =
    map-inv-equiv (extensionality-equiv-Cyclic-Type e f)

comp-equiv-Cyclic-Type :
  {l1 l2 l3 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k)
  (Z : Cyclic-Type l3 k) 
  equiv-Cyclic-Type k Y Z  equiv-Cyclic-Type k X Y  equiv-Cyclic-Type k X Z
comp-equiv-Cyclic-Type k X Y Z =
  comp-equiv-Endo
    ( endo-Cyclic-Type k X)
    ( endo-Cyclic-Type k Y)
    ( endo-Cyclic-Type k Z)

inv-equiv-Cyclic-Type :
  {l1 l2 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) 
  equiv-Cyclic-Type k X Y  equiv-Cyclic-Type k Y X
inv-equiv-Cyclic-Type k X Y =
  inv-equiv-Endo (endo-Cyclic-Type k X) (endo-Cyclic-Type k Y)

associative-comp-equiv-Cyclic-Type :
  {l1 l2 l3 l4 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k)
  (Z : Cyclic-Type l3 k) (W : Cyclic-Type l4 k) (g : equiv-Cyclic-Type k Z W)
  (f : equiv-Cyclic-Type k Y Z) (e : equiv-Cyclic-Type k X Y) 
  Id
    ( comp-equiv-Cyclic-Type
        k X Y W (comp-equiv-Cyclic-Type k Y Z W g f) e)
    ( comp-equiv-Cyclic-Type
        k X Z W g (comp-equiv-Cyclic-Type k X Y Z f e))
associative-comp-equiv-Cyclic-Type k X Y Z W g f e =
  eq-htpy-equiv-Cyclic-Type k X W
    ( comp-equiv-Cyclic-Type
        k X Y W (comp-equiv-Cyclic-Type k Y Z W g f) e)
    ( comp-equiv-Cyclic-Type
        k X Z W g (comp-equiv-Cyclic-Type k X Y Z f e))
    ( refl-htpy)

module _
  {l1 l2 : Level} (k : ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k)
  (e : equiv-Cyclic-Type k X Y)
  where

  left-unit-law-comp-equiv-Cyclic-Type :
    Id (comp-equiv-Cyclic-Type k X Y Y (id-equiv-Cyclic-Type k Y) e) e
  left-unit-law-comp-equiv-Cyclic-Type =
    eq-htpy-equiv-Cyclic-Type k X Y
      ( comp-equiv-Cyclic-Type k X Y Y (id-equiv-Cyclic-Type k Y) e)
      ( e)
      ( refl-htpy)

  right-unit-law-comp-equiv-Cyclic-Type :
    Id (comp-equiv-Cyclic-Type k X X Y e (id-equiv-Cyclic-Type k X)) e
  right-unit-law-comp-equiv-Cyclic-Type =
    eq-htpy-equiv-Cyclic-Type k X Y
      ( comp-equiv-Cyclic-Type k X X Y e (id-equiv-Cyclic-Type k X))
      ( e)
      ( refl-htpy)

  left-inverse-law-comp-equiv-Cyclic-Type :
    Id ( comp-equiv-Cyclic-Type k X Y X (inv-equiv-Cyclic-Type k X Y e) e)
       ( id-equiv-Cyclic-Type k X)
  left-inverse-law-comp-equiv-Cyclic-Type =
    eq-htpy-equiv-Cyclic-Type k X X
      ( comp-equiv-Cyclic-Type k X Y X (inv-equiv-Cyclic-Type k X Y e) e)
      ( id-equiv-Cyclic-Type k X)
      ( isretr-map-inv-equiv (equiv-equiv-Cyclic-Type k X Y e))

  right-inverse-law-comp-equiv-Cyclic-Type :
    Id ( comp-equiv-Cyclic-Type k Y X Y e (inv-equiv-Cyclic-Type k X Y e))
       ( id-equiv-Cyclic-Type k Y)
  right-inverse-law-comp-equiv-Cyclic-Type =
    eq-htpy-equiv-Cyclic-Type k Y Y
      ( comp-equiv-Cyclic-Type k Y X Y e (inv-equiv-Cyclic-Type k X Y e))
      ( id-equiv-Cyclic-Type k Y)
      ( issec-map-inv-equiv (equiv-equiv-Cyclic-Type k X Y e))

mere-eq-Cyclic-Type : {l : Level} (k : ) (X Y : Cyclic-Type l k)  mere-eq X Y
mere-eq-Cyclic-Type k X Y =
  apply-universal-property-trunc-Prop
    ( mere-equiv-endo-Cyclic-Type k X)
    ( mere-eq-Prop X Y)
    ( λ e 
      apply-universal-property-trunc-Prop
        ( mere-equiv-endo-Cyclic-Type k Y)
        ( mere-eq-Prop X Y)
        ( λ f 
          unit-trunc-Prop
            ( eq-equiv-Cyclic-Type k X Y
              ( comp-equiv-Cyclic-Type k X (ℤ-Mod-Cyclic-Type k) Y f
                ( inv-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X e)))))

is-0-connected-Cyclic-Type :
  (k : )  is-0-connected (Cyclic-Type lzero k)
is-0-connected-Cyclic-Type k =
  is-0-connected-mere-eq
    ( ℤ-Mod-Cyclic-Type k)
    ( mere-eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k))

∞-group-Cyclic-Type :
  (k : )  ∞-Group (lsuc lzero)
pr1 (∞-group-Cyclic-Type k) = Cyclic-Type-Pointed-Type k
pr2 (∞-group-Cyclic-Type k) = is-0-connected-Cyclic-Type k

Eq-Cyclic-Type : (k : )  Cyclic-Type lzero k  UU lzero
Eq-Cyclic-Type k X = type-Cyclic-Type k X

refl-Eq-Cyclic-Type : (k : )  Eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k)
refl-Eq-Cyclic-Type k = zero-ℤ-Mod k

Eq-equiv-Cyclic-Type :
  (k : ) (X : Cyclic-Type lzero k) 
  equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X  Eq-Cyclic-Type k X
Eq-equiv-Cyclic-Type k X e =
  map-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X e (zero-ℤ-Mod k)

equiv-Eq-Cyclic-Type :
  (k : )  Eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) 
  equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k)
pr1 (equiv-Eq-Cyclic-Type k x) = equiv-add-ℤ-Mod' k x
pr2 (equiv-Eq-Cyclic-Type k x) y = left-successor-law-add-ℤ-Mod k y x

issec-equiv-Eq-Cyclic-Type :
  (k : ) 
  (Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k)  equiv-Eq-Cyclic-Type k) ~ id
issec-equiv-Eq-Cyclic-Type zero-ℕ x = left-unit-law-add-ℤ x
issec-equiv-Eq-Cyclic-Type (succ-ℕ k) x = left-unit-law-add-Fin k x

preserves-pred-preserves-succ-map-ℤ-Mod :
  (k : ) (f : ℤ-Mod k  ℤ-Mod k) 
  (f  succ-ℤ-Mod k) ~ (succ-ℤ-Mod k  f) 
  (f  pred-ℤ-Mod k) ~ (pred-ℤ-Mod k  f)
preserves-pred-preserves-succ-map-ℤ-Mod k f H x =
  ( inv (isretr-pred-ℤ-Mod k (f (pred-ℤ-Mod k x)))) 
  ( ap
    ( pred-ℤ-Mod k)
    ( ( inv (H (pred-ℤ-Mod k x))) 
      ( ap f (issec-pred-ℤ-Mod k x))))

compute-map-preserves-succ-map-ℤ-Mod' :
  (k : ) (f : ℤ-Mod k  ℤ-Mod k)  (f  succ-ℤ-Mod k) ~ (succ-ℤ-Mod k  f) 
  (x : )  Id (add-ℤ-Mod k (mod-ℤ k x) (f (zero-ℤ-Mod k))) (f (mod-ℤ k x))
compute-map-preserves-succ-map-ℤ-Mod' k f H (inl zero-ℕ) =
  ( ap (add-ℤ-Mod' k (f (zero-ℤ-Mod k))) (mod-neg-one-ℤ k)) 
  ( ( inv (is-left-add-neg-one-pred-ℤ-Mod k (f (zero-ℤ-Mod k)))) 
    ( ( ap (pred-ℤ-Mod k) (ap f (inv (mod-zero-ℤ k)))) 
      ( ( inv
          ( preserves-pred-preserves-succ-map-ℤ-Mod k f H (mod-ℤ k zero-ℤ))) 
        ( inv (ap f (preserves-predecessor-mod-ℤ k zero-ℤ))))))
compute-map-preserves-succ-map-ℤ-Mod' k f H (inl (succ-ℕ x)) =
  ( ap
    ( add-ℤ-Mod' k (f (zero-ℤ-Mod k)))
    ( preserves-predecessor-mod-ℤ k (inl x))) 
  ( ( left-predecessor-law-add-ℤ-Mod k (mod-ℤ k (inl x)) (f (zero-ℤ-Mod k))) 
    ( ( ap
        ( pred-ℤ-Mod k)
        ( compute-map-preserves-succ-map-ℤ-Mod' k f H (inl x))) 
      ( ( inv
          ( preserves-pred-preserves-succ-map-ℤ-Mod k f H (mod-ℤ k (inl x)))) 
        ( ap f (inv (preserves-predecessor-mod-ℤ k (inl x)))))))
compute-map-preserves-succ-map-ℤ-Mod' k f H (inr (inl star)) =
  ( ap (add-ℤ-Mod' k (f (zero-ℤ-Mod k))) (mod-zero-ℤ k)) 
  ( ( left-unit-law-add-ℤ-Mod k (f (zero-ℤ-Mod k))) 
    ( ap f (inv (mod-zero-ℤ k))))
compute-map-preserves-succ-map-ℤ-Mod' k f H (inr (inr zero-ℕ)) =
  ( ap-add-ℤ-Mod k (mod-one-ℤ k) (ap f (inv (mod-zero-ℤ k)))) 
  ( ( inv (is-left-add-one-succ-ℤ-Mod k (f (mod-ℤ k zero-ℤ)))) 
    ( ( inv (H (mod-ℤ k zero-ℤ))) 
      ( ap f (inv (preserves-successor-mod-ℤ k zero-ℤ)))))
compute-map-preserves-succ-map-ℤ-Mod' k f H (inr (inr (succ-ℕ x))) =
  ( ap
    ( add-ℤ-Mod' k (f (zero-ℤ-Mod k)))
    ( preserves-successor-mod-ℤ k (inr (inr x)))) 
  ( ( left-successor-law-add-ℤ-Mod k
      ( mod-ℤ k (inr (inr x)))
      ( f (zero-ℤ-Mod k))) 
    ( ( ap
        ( succ-ℤ-Mod k)
        ( compute-map-preserves-succ-map-ℤ-Mod' k f H (inr (inr x)))) 
      ( ( inv (H (mod-ℤ k (inr (inr x))))) 
        ( ap f (inv (preserves-successor-mod-ℤ k (inr (inr x))))))))

compute-map-preserves-succ-map-ℤ-Mod :
  (k : ) (f : ℤ-Mod k  ℤ-Mod k) (H : (f  succ-ℤ-Mod k) ~ (succ-ℤ-Mod k  f))
  (x : ℤ-Mod k)  Id (add-ℤ-Mod k x (f (zero-ℤ-Mod k))) (f x)
compute-map-preserves-succ-map-ℤ-Mod k f H x =
  ( ap (add-ℤ-Mod' k (f (zero-ℤ-Mod k))) (inv (issec-int-ℤ-Mod k x))) 
  ( ( compute-map-preserves-succ-map-ℤ-Mod' k f H (int-ℤ-Mod k x)) 
    ( ap f (issec-int-ℤ-Mod k x)))

isretr-equiv-Eq-Cyclic-Type :
  (k : ) 
  (equiv-Eq-Cyclic-Type k  Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k)) ~ id
isretr-equiv-Eq-Cyclic-Type k e =
  eq-htpy-equiv-Cyclic-Type k
    ( ℤ-Mod-Cyclic-Type k)
    ( ℤ-Mod-Cyclic-Type k)
    ( equiv-Eq-Cyclic-Type k (Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) e))
    ( e)
    ( compute-map-preserves-succ-map-ℤ-Mod
      ( k)
      ( map-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k) e)
      ( coherence-square-equiv-Cyclic-Type
        ( k)
        ( ℤ-Mod-Cyclic-Type k)
        ( ℤ-Mod-Cyclic-Type k)
        ( e)))

is-equiv-Eq-equiv-Cyclic-Type :
  (k : ) (X : Cyclic-Type lzero k)  is-equiv (Eq-equiv-Cyclic-Type k X)
is-equiv-Eq-equiv-Cyclic-Type k X =
  apply-universal-property-trunc-Prop
    ( mere-eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X)
    ( is-equiv-Prop (Eq-equiv-Cyclic-Type k X))
    ( λ { refl 
          is-equiv-has-inverse
            ( equiv-Eq-Cyclic-Type k)
            ( issec-equiv-Eq-Cyclic-Type k)
            ( isretr-equiv-Eq-Cyclic-Type k)})

equiv-compute-Ω-Cyclic-Type :
  (k : )  type-Ω (pair (Cyclic-Type lzero k) (ℤ-Mod-Cyclic-Type k))  ℤ-Mod k
equiv-compute-Ω-Cyclic-Type k =
  ( pair
    ( Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k))
    ( is-equiv-Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k))) ∘e
  ( extensionality-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k))

map-equiv-compute-Ω-Cyclic-Type :
  (k : )  type-Ω (pair (Cyclic-Type lzero k) (ℤ-Mod-Cyclic-Type k))  ℤ-Mod k
map-equiv-compute-Ω-Cyclic-Type k = map-equiv (equiv-compute-Ω-Cyclic-Type k)

preserves-concat-equiv-eq-Cyclic-Type :
  (k : ) (X Y Z : Cyclic-Type lzero k) (p : Id X Y) (q : Id Y Z) 
  Id ( equiv-eq-Cyclic-Type k X Z (p  q))
     ( comp-equiv-Cyclic-Type k X Y Z
       ( equiv-eq-Cyclic-Type k Y Z q)
       ( equiv-eq-Cyclic-Type k X Y p))
preserves-concat-equiv-eq-Cyclic-Type k X .X Z refl q =
  inv
    ( right-unit-law-comp-equiv-Cyclic-Type
        k X Z (equiv-eq-Cyclic-Type k X Z q))

preserves-comp-Eq-equiv-Cyclic-Type :
  (k : )
  (e f : equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k)) 
  Id ( Eq-equiv-Cyclic-Type k
       ( ℤ-Mod-Cyclic-Type k)
       ( comp-equiv-Cyclic-Type k
         ( ℤ-Mod-Cyclic-Type k)
         ( ℤ-Mod-Cyclic-Type k)
         ( ℤ-Mod-Cyclic-Type k)
         ( f)
         ( e)))
     ( add-ℤ-Mod k
       ( Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) e)
       ( Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) f))
preserves-comp-Eq-equiv-Cyclic-Type k e f =
  inv
  ( compute-map-preserves-succ-map-ℤ-Mod k
    ( map-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k) f)
    ( coherence-square-equiv-Cyclic-Type k
      ( ℤ-Mod-Cyclic-Type k)
      ( ℤ-Mod-Cyclic-Type k)
      ( f))
    ( map-equiv-Cyclic-Type k
      ( ℤ-Mod-Cyclic-Type k)
      ( ℤ-Mod-Cyclic-Type k)
      ( e)
      ( zero-ℤ-Mod k)))

preserves-concat-equiv-compute-Ω-Cyclic-Type :
  (k : ) (p q : type-Ω (Cyclic-Type-Pointed-Type k)) 
  Id ( map-equiv (equiv-compute-Ω-Cyclic-Type k) (p  q))
     ( add-ℤ-Mod k
       ( map-equiv (equiv-compute-Ω-Cyclic-Type k) p)
       ( map-equiv (equiv-compute-Ω-Cyclic-Type k) q))
preserves-concat-equiv-compute-Ω-Cyclic-Type k p q =
  ( ap
    ( Eq-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k))
    ( preserves-concat-equiv-eq-Cyclic-Type k
      ( ℤ-Mod-Cyclic-Type k)
      ( ℤ-Mod-Cyclic-Type k)
      ( ℤ-Mod-Cyclic-Type k)
      ( p)
      ( q))) 
  ( preserves-comp-Eq-equiv-Cyclic-Type k
    ( equiv-eq-Cyclic-Type k ( ℤ-Mod-Cyclic-Type k) ( ℤ-Mod-Cyclic-Type k) p)
    ( equiv-eq-Cyclic-Type k ( ℤ-Mod-Cyclic-Type k) ( ℤ-Mod-Cyclic-Type k) q))

type-Ω-Cyclic-Type : (k : )  UU (lsuc lzero)
type-Ω-Cyclic-Type k = Id (ℤ-Mod-Cyclic-Type k) (ℤ-Mod-Cyclic-Type k)

is-set-type-Ω-Cyclic-Type : (k : )  is-set (type-Ω-Cyclic-Type k)
is-set-type-Ω-Cyclic-Type k =
  is-set-equiv
    ( ℤ-Mod k)
    ( equiv-compute-Ω-Cyclic-Type k)
    ( is-set-ℤ-Mod k)

concrete-group-Cyclic-Type :
  (k : )  Concrete-Group (lsuc lzero)
pr1 (concrete-group-Cyclic-Type k) = ∞-group-Cyclic-Type k
pr2 (concrete-group-Cyclic-Type k) = is-set-type-Ω-Cyclic-Type k

Ω-Cyclic-Type-Group : (k : )  Group (lsuc lzero)
Ω-Cyclic-Type-Group k =
  loop-space-Group
    ( pair (Cyclic-Type lzero k) (ℤ-Mod-Cyclic-Type k))
    ( is-set-type-Ω-Cyclic-Type k)

equiv-Ω-Cyclic-Type-Group :
  (k : )  equiv-Group (Ω-Cyclic-Type-Group k) (ℤ-Mod-Group k)
pr1 (equiv-Ω-Cyclic-Type-Group k) = equiv-compute-Ω-Cyclic-Type k
pr2 (equiv-Ω-Cyclic-Type-Group k) =
  preserves-concat-equiv-compute-Ω-Cyclic-Type k

iso-Ω-Cyclic-Type-Group :
  (k : )  type-iso-Group (Ω-Cyclic-Type-Group k) (ℤ-Mod-Group k)
iso-Ω-Cyclic-Type-Group k =
  iso-equiv-Group
    ( Ω-Cyclic-Type-Group k)
    ( ℤ-Mod-Group k)
    ( equiv-Ω-Cyclic-Type-Group k)