# Types equipped with automorphisms

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-06-29.

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