# Sets equipped with automorphisms

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-08.

module structured-types.sets-equipped-with-automorphisms where

Imports
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.sets
open import foundation.universe-levels


## Idea

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

## Definitions

### Sets equipped with automorphisms

Set-With-Automorphism : (l : Level) → UU (lsuc l)
Set-With-Automorphism l = Σ (Set l) (Aut ∘ type-Set)

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

set-Set-With-Automorphism : Set l
set-Set-With-Automorphism = pr1 A

type-Set-With-Automorphism : UU l
type-Set-With-Automorphism = type-Set set-Set-With-Automorphism

is-set-type-Set-With-Automorphism : is-set type-Set-With-Automorphism
is-set-type-Set-With-Automorphism = is-set-type-Set set-Set-With-Automorphism

aut-Set-With-Automorphism : Aut type-Set-With-Automorphism
aut-Set-With-Automorphism = pr2 A

map-Set-With-Automorphism :
type-Set-With-Automorphism → type-Set-With-Automorphism
map-Set-With-Automorphism = map-equiv aut-Set-With-Automorphism