Cyclic types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.
Last modified on 2023-11-24.

module structured-types.cyclic-types where
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.iterating-automorphisms
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.surjective-maps
open import foundation.universe-levels

open import structured-types.sets-equipped-with-automorphisms


A cyclic set consists of a set A equipped with an automorphism e : A ≃ A which is cyclic in the sense that its underlying set is inhabited and the map

  k ↦ eᵏ x

is surjective for every x : A. There are several equivalent ways of stating the concept of cyclic sets. Two further equivalent ways are:

Note that the empty set equipped with the identity automorphism is not considered to be a cyclic set, for reasons similar to those of not considering empty group actions to be transitive.


The predicate of being a cyclic set

module _
  {l : Level} (X : Set-With-Automorphism l)

  is-cyclic-prop-Set-With-Automorphism : Prop l
  is-cyclic-prop-Set-With-Automorphism =
      ( trunc-Prop (type-Set-With-Automorphism X))
      ( Π-Prop
        ( type-Set-With-Automorphism X)
        ( λ x 
            ( λ k 
              map-iterate-automorphism-ℤ k (aut-Set-With-Automorphism X) x)))

  is-cyclic-Set-With-Automorphism : UU l
  is-cyclic-Set-With-Automorphism =
    type-Prop is-cyclic-prop-Set-With-Automorphism

Cyclic sets

Cyclic-Set :
  (l : Level)  UU (lsuc l)
Cyclic-Set l =
  Σ (Set-With-Automorphism l)  X  is-cyclic-Set-With-Automorphism X)

module _
  {l : Level} (X : Cyclic-Set l)

  set-with-automorphism-Cyclic-Set : Set-With-Automorphism l
  set-with-automorphism-Cyclic-Set = pr1 X

  set-Cyclic-Set : Set l
  set-Cyclic-Set = set-Set-With-Automorphism set-with-automorphism-Cyclic-Set

  type-Cyclic-Set : UU l
  type-Cyclic-Set = type-Set-With-Automorphism set-with-automorphism-Cyclic-Set

  is-set-type-Cyclic-Set : is-set type-Cyclic-Set
  is-set-type-Cyclic-Set =
    is-set-type-Set-With-Automorphism set-with-automorphism-Cyclic-Set

  aut-Cyclic-Set : Aut type-Cyclic-Set
  aut-Cyclic-Set = aut-Set-With-Automorphism set-with-automorphism-Cyclic-Set

  map-Cyclic-Set : type-Cyclic-Set  type-Cyclic-Set
  map-Cyclic-Set = map-Set-With-Automorphism set-with-automorphism-Cyclic-Set

See also

Recent changes