Furstenberg groups
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-03-12.
Last modified on 2023-03-15.
module group-theory.furstenberg-groups where
Imports
open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.propositional-truncations open import foundation.sets open import foundation.universe-levels
Definition
Furstenberg-Group : (l : Level) → UU (lsuc l) Furstenberg-Group l = Σ ( Set l) ( λ X → ( type-trunc-Prop (type-Set X)) × ( Σ ( type-Set X → type-Set X → type-Set X) ( λ μ → ( (x y z : type-Set X) → Id (μ (μ x z) (μ y z)) (μ x y)) × ( Σ ( type-Set X → type-Set X → type-Set X) ( λ δ → (x y : type-Set X) → Id (μ x (δ x y)) y)))))
Recent changes
- 2023-03-15. Fredrik Bakke. Remove blank lines at the start and end of code blocks (#508).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
- 2023-03-05. Jonathan Prieto-Cubides. Add "suggest an edit" button and minor fix (#484).