Types equipped with automorphisms
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-06-29.
Last modified on 2023-06-08.
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
Idea
A type equipped with an automorphism is a pair consisting of a type A
and an
automorphism on A
.
Definition
Type-Aut : (l : Level) → UU (lsuc l) Type-Aut l = Σ (UU l) (Aut) type-Type-Aut : {l : Level} → Type-Aut l → UU l type-Type-Aut (X , e) = X aut-Type-Aut : {l : Level} (A : Type-Aut l) → Aut (type-Type-Aut A) aut-Type-Aut (X , e) = e
Properties
Every type can be equipped with the identity automorpism
id-Type-Aut : {l : Level} → UU l → Type-Aut l pr1 (id-Type-Aut X) = X pr2 (id-Type-Aut X) = id-equiv
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).