# Types equipped with automorphisms ```agda module structured-types.types-equipped-with-automorphisms where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea A **type equipped with an automorphism** is a pair consisting of a type `A` and an [automorphism](foundation.automorphisms.md) on `e : A ≃ A`. ## Definitions ### Types equipped with automorphisms ```agda 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 ```agda 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 - Sets equipped with automorphisms are defined in [`structured-types.sets-equipped-with-automorphisms.md`](structured-types.sets-equipped-with-automorphisms.md) - Cyclic types are [sets equipped with automorphisms](structured-types.sets-equipped-with-automorphisms.md) of which the automorphism acts transitively. - The [descent property of the circle](synthetic-homotopy-theory.descent-circle.md) shows that type families over the [circle](synthetic-homotopy-theory.circle.md) are [equivalently](foundation.equivalences.md) described as types equipped with automorphisms.