27 lines
1,010 B
Agda
27 lines
1,010 B
Agda
open import Level
|
||
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
|
||
|
||
module Algebra.Group where
|
||
record IsGroup {ℓ} (A : Set ℓ) (_∙_ : A → A → A) (ε : A) (_⁻¹ : A → A) : Set (suc ℓ) where
|
||
field
|
||
assoc : ∀ {f g h : A} → (f ∙ g) ∙ h ≡ f ∙ (g ∙ h)
|
||
idˡ : ∀ {g : A} → ε ∙ g ≡ g
|
||
idʳ : ∀ {g : A} → g ∙ ε ≡ g
|
||
invˡ : ∀ {g : A} → g ∙ (g ⁻¹) ≡ ε
|
||
invʳ : ∀ {g : A} → (g ⁻¹) ∙ g ≡ ε
|
||
|
||
record Group (ℓ : Level) : Set (suc ℓ) where
|
||
infix 8 _⁻¹
|
||
infixl 7 _∙_
|
||
field
|
||
Carrier : Set ℓ
|
||
_∙_ : Carrier → Carrier → Carrier
|
||
ε : Carrier
|
||
_⁻¹ : Carrier → Carrier
|
||
|
||
field
|
||
isGroup : IsGroup Carrier _∙_ ε _⁻¹
|
||
open IsGroup isGroup public
|
||
|
||
∙-resp : ∀ {f h g i : Carrier} → f ≡ h → g ≡ i → f ∙ g ≡ h ∙ i
|
||
∙-resp {f} {h} {g} {i} f≡h g≡i = ≡.trans (≡.cong (f ∙_) g≡i) (≡.cong (_∙ i) f≡h)
|