Groups and family 2

Here we define the objects based on the conditions defined in the previous section. It might be helpful here to think of `Data` fields as datatypes as used in computer sciences, and the objects as the structure defined on operations of that datatype. For e.g. if a datatype’s equivalence (or equality evaluator) happens to be congruent, then the datatype and its equivalence relation form a “magma”. Thus the object itself encodes the relationship of a datatype with an operation.

Such structures can often be applied in computer science in curious ways, such as using the monoidal functions (μ: T → T → T) for reduce operations (part of “map-reduce” in big data), progressively “reducing” a large quantity of `T`s into one final value of type `T`, e.g. addition of an enormous list of numbers. Monoids, Groups and Semigroups form the basis for an arguably large number of patterns especially in functional programming.

``````module Algebra.groups2 where

open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)

open import Types.equality using (Rel)
open import Algebra.groups``````

We recall operations again here:

``````★_ : ∀ {a} → Set a → Set a
★ A = A → A → A

♠_ : ∀ {a} → Set a → Set a
♠ A = A → A``````

Magma

``````record Magma a ℓ : Set (lsuc (a ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data      : Set a
_==_       : Rel Data ℓ
_∙_       : ★ Data
isMagma   : IsMagma _==_ _∙_

open IsMagma isMagma public``````

Semigroupoid

``````record Semigroupoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data            : Set c
_==_            : Rel Data ℓ
_∙_             : ★ Data
isSemigroupoid  : IsSemigroupoid _==_ _∙_

open IsSemigroupoid isSemigroupoid public``````

Small category

``````record SmallCategory c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data            : Set c
_==_            : Rel Data ℓ
_∙_             : ★ Data
ε               : Data
isSmallCategory : IsSmallCategory _==_ _∙_ ε

open IsSmallCategory isSmallCategory public

semigroupoid : Semigroupoid c ℓ
semigroupoid = record { isSemigroupoid = isSemigroupoid }``````

Semigroup

Semigroups can be used in functional programming to abstract over associative operations for non-trivial datatypes, such as “adding” two dictionatries or “multiplying” a character (repeating it n times), etc.

``````record Semigroup c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data        : Set c
_==_        : Rel Data ℓ
_∙_         : ★ Data
isSemigroup : IsSemigroup _==_ _∙_

open IsSemigroup isSemigroup public

magma : Magma c ℓ
magma = record { isMagma = isMagma }``````

Groupoid

``````record Groupoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data            : Set c
_==_            : Rel Data ℓ
_∙_             : ★ Data
ε               : Data
_⁻¹             : ♠ Data
isGroupoid      : IsGroupoid _==_ _∙_ ε _⁻¹

open IsGroupoid isGroupoid public

smallcategory : SmallCategory c ℓ
smallcategory = record { isSmallCategory = isSmallCategory }

semigroupoid : Semigroupoid c ℓ
semigroupoid = record { isSemigroupoid = isSemigroupoid }``````

Monoid

``````record Monoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data     : Set c
_==_      : Rel Data ℓ
_∙_      : ★ Data
ε        : Data
isMonoid : IsMonoid _==_ _∙_ ε

open IsMonoid isMonoid public

semigroup : Semigroup c ℓ
semigroup = record { isSemigroup = isSemigroup }

magma : Magma c ℓ
magma = record { isMagma = isMagma }``````

Commutative Monoid

``````record CommutativeMonoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infixl 7 _∙_
infix  4 _==_
field
Data                : Set c
_==_                 : Rel Data ℓ
_∙_                 : ★ Data
ε                   : Data
isCommutativeMonoid : IsCommutativeMonoid _==_ _∙_ ε

open IsCommutativeMonoid isCommutativeMonoid public

monoid : Monoid c ℓ
monoid = record { isMonoid = isMonoid }

semigroup : Semigroup c ℓ
semigroup = record { isSemigroup = isSemigroup }

magma : Magma c ℓ
magma = record { isMagma = isMagma }``````

Group

``````record Group c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix  8 _⁻¹
infixl 7 _∙_
infix  4 _==_
field
Data    : Set c
_==_    : Rel Data ℓ
_∙_     : ★ Data
ε       : Data
_⁻¹     : ♠ Data
isGroup : IsGroup _==_ _∙_ ε _⁻¹

open IsGroup isGroup public

monoid : Monoid _ _
monoid = record { isMonoid = isMonoid }

semigroup : Semigroup c ℓ
semigroup = record { isSemigroup = isSemigroup }

magma : Magma c ℓ
magma = record { isMagma = isMagma }``````

Abelian Group

``````open import Algebra.groups using (IsAbelianGroup)

record AbelianGroup c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix  8 _⁻¹
infixl 7 _∙_
infix  4 _==_
field
Data           : Set c
_==_            : Rel Data ℓ
_∙_            : ★ Data
ε              : Data
_⁻¹            : ♠ Data
isAbelianGroup : IsAbelianGroup _==_ _∙_ ε _⁻¹

open IsAbelianGroup isAbelianGroup public

group : Group c ℓ
group = record { isGroup = isGroup }

monoid : Monoid _ _
monoid = record { isMonoid = isMonoid }

semigroup : Semigroup c ℓ
semigroup = record { isSemigroup = isSemigroup }

magma : Magma c ℓ
magma = record { isMagma = isMagma }``````

Group Morphisms