Types equipped with endomorphisms
Content created by Jonathan Prieto-Cubides, Egbert Rijke, Fredrik Bakke and Victor Blanchi.
Created on 2022-05-07.
Last modified on 2023-06-24.
module structured-types.types-equipped-with-endomorphisms where
Imports
open import foundation.dependent-pair-types open import foundation.endomorphisms open import foundation.function-types open import foundation.unit-type open import foundation.universe-levels
Idea
A type equipped with an endomorphism consists of a type A
equipped with a map
A → A
.
Definitions
Types equipped with endomorphisms
Endo : (l : Level) → UU (lsuc l) Endo l = Σ (UU l) endo module _ {l : Level} (X : Endo l) where type-Endo : UU l type-Endo = pr1 X endomorphism-Endo : type-Endo → type-Endo endomorphism-Endo = pr2 X
Example
Unit type equipped with endomorphisms
trivial-Endo : {l : Level} → Endo l pr1 (trivial-Endo {l}) = raise-unit l pr2 trivial-Endo = id
Recent changes
- 2023-06-24. Fredrik Bakke. Whitespace after closing braces and before opening braces (#671).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-10. Victor Blanchi. Iterated cartesian products of concrete groups (#566).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).