Contents Previous Next


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 Ts 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