This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Types equipped with automorphisms

module structured-types.types-equipped-with-automorphisms where
Imports 
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels

open import structured-types.types-equipped-with-endomorphisms

Idea

A type equipped with an automorphism is a pair consisting of a type A and an automorphism on e : A ≃ A.

Definitions

Types equipped with automorphisms

Type-With-Automorphism : (l : Level) → UU (lsuc l)
Type-With-Automorphism l = Σ (UU l) (Aut)

module _
  {l : Level} (A : Type-With-Automorphism l)
  where

  type-Type-With-Automorphism : UU l
  type-Type-With-Automorphism = pr1 A

  automorphism-Type-With-Automorphism : Aut type-Type-With-Automorphism
  automorphism-Type-With-Automorphism = pr2 A

  map-Type-With-Automorphism :
    type-Type-With-Automorphism → type-Type-With-Automorphism
  map-Type-With-Automorphism = map-equiv automorphism-Type-With-Automorphism

  type-with-endomorphism-Type-With-Automorphism : Type-With-Endomorphism l
  pr1 type-with-endomorphism-Type-With-Automorphism =
    type-Type-With-Automorphism
  pr2 type-with-endomorphism-Type-With-Automorphism =
    map-Type-With-Automorphism

Types equipped with the identity automorphism

trivial-Type-With-Automorphism : {l : Level} → UU l → Type-With-Automorphism l
pr1 (trivial-Type-With-Automorphism X) = X
pr2 (trivial-Type-With-Automorphism X) = id-equiv

See also