Sheargroups

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) → Id (m e x) x) ×
              ( ( (x : type-Set X) → Id (m x x) e) ×
                ( (x y z : type-Set X) →
                  Id (m x (m y z)) (m (m (m x (m y e)) e) z))))))