Sheargroups

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

Created on 2022-03-12.
Last modified on 2025-10-17.

module group-theory.sheargroups where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

Definition

Sheargroup : (l : Level) → UU (lsuc l)
Sheargroup l =
  Σ ( Set l)
    ( λ X →
      Σ ( type-Set X)
        ( λ e →
          Σ (type-Set X → type-Set X → type-Set X)
            ( λ m →
              ( (x : type-Set X) → m e x ＝ x) ×
              ( ( (x : type-Set X) → m x x ＝ e) ×
                ( (x y z : type-Set X) →
                  m x (m y z) ＝ m (m (m x (m y e)) e) z)))))

Recent changes