Definition. 群 Group [Group.Def]

module Group.Def where

open import MLTT.Spartan hiding (_∙_) renaming (_⁻¹ to sym)
open import UF.Base
open import UF.Sets
open import UF.Sets-Properties

一個群（group）是由一個非空集合 G 跟一個二元運算子（binary operation）

• : G × G → G

構成，且滿足以下條件

1. G 有一個特別的元素叫單位元素（identity 或是 neutral element），用 e 表示，任何元素 g 跟它運算都是 g，也就是 g = g • e = e • g
2. 這個運算子是 associative 的，也就是說 (a • b) • c = a • (b • c)，所以我們可以安全的寫成 a • b • c
3. 每個元素 g ∈ G 都有一個反元素 g⁻¹ ∈ G，滿足以下等式 g • g⁻¹ = g⁻¹ • g = e

我們把這些條件匯總，就寫成了下面的定義

record Group (G : 𝓤 ̇) : 𝓤 ̇ where
  field
    size : is-set G
    _∙_ : G → G → G
    ∙-assoc : associative _∙_
    e : G
    neu-l : left-neutral e _∙_
    neu-r : right-neutral e _∙_
    _⁻¹ : G → G
    cancel : {x : G} → ((x ⁻¹) ∙ x ＝ e) × (x ∙ (x ⁻¹) ＝ e)

  infix  _⁻¹
  infixl  _∙_