```
module Application.Algebra where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; setoid)

import Relation.Binary.EqReasoning as EqR```

# Semigroup property

Let `A` be a type and let `_∙_` be a binary operation on `A`. `A` with `_∙_` forms a semigroup iff `_∙_` is associative.

We can model the semigroup proposition as follows:

```
record IsSemigroup {A : Set} (_∙_ : A → A → A) : Set where
field
assoc         : ∀ x y z →  ((x ∙ y) ∙ z)  ≡  (x ∙ (y ∙ z))```

# Exercise

Prove that `ℕ` with `_+_` forms a semigroup!

```
ℕ+-isSemigroup : IsSemigroup _+_```

# Usage

Usage example:

```
module Usage₁ where
open IsSemigroup

ex : ∀ n → (n + 1) + 1 ≡ n + 2
ex n = assoc ℕ+-isSemigroup n 1 1```

With applied module opening:

```
module Usage₂ where
open IsSemigroup ℕ+-isSemigroup

ex : ∀ n → (n + 1) + 1 ≡ n + 2
ex n = assoc n 1 1```

With local module opening:

```
module Usage₃ where
ex : ∀ n → (n + 1) + 1 ≡ n + 2
ex n = assoc n 1 1  where
open IsSemigroup ℕ+-isSemigroup```

# Monoid property

`IsMonoid {A} _∙_ ε` represents the proposition that (`A`, `_∙_`, `ε`) is a monoid:

```
record IsMonoid {A : Set} (_∙_ : A → A → A) (ε : A) : Set where
field
isSemigroup : IsSemigroup _∙_
identity    : (∀ x → (ε ∙ x) ≡ x)  ×  (∀ x → (x ∙ ε) ≡ x)

open IsSemigroup isSemigroup public```

Public opening at the end makes usage of `IsMonoid` easier.

# Exercise

Prove that (`ℕ`, `_+_`, `0`) forms a monoid!

```
ℕ+0-isMonoid : IsMonoid _+_ 0```

# Usage

Usage example:

```
module Usage₄ where
ex : ∀ n → (n + 0) + n ≡ n + n
ex n = cong (λ x → x + n) (proj₂ identity n)  where
open IsMonoid ℕ+0-isMonoid

ex′ : ∀ n → (n + 0) + n ≡ n + n
ex′ n = assoc n 0 n  where
open IsMonoid ℕ+0-isMonoid   -- we opened IsMonoid, not IsSemigroup```

# Named binary operations

Instead of `A → A → A` we can write `Op₂ A` if we define

```
Op₂ : Set → Set
Op₂ A = A → A → A```

Thus we can write

```
record IsSemigroup′ {A : Set} (_∙_ : Op₂ A) : Set where
field
assoc         : ∀ x y z →  ((x ∙ y) ∙ z)  ≡  (x ∙ (y ∙ z))```

# Exercise

Define the type of unary operations as `Op₁`!

# Named function properties

We can name functions properties like

```
Associative : {A : Set} → Op₂ A → Set
Associative _∙_ = ∀ x y z →  ((x ∙ y) ∙ z)  ≡  (x ∙ (y ∙ z))```

After this definition we can write

```
record IsSemigroup″ {A : Set} (_∙_ : Op₂ A) : Set where
field
assoc         : Associative _∙_```

# Exercises

Define the following function properties!

```
Commutative : {A : Set} → Op₂ A → Set _```

The first parameter of `LeftIdentity` is the neutral element.

```
LeftIdentity : {A : Set} → A → Op₂ A → Set _```

```
RightIdentity : {A : Set} → A → Op₂ A → Set _```

```
Identity : {A : Set} → A → Op₂ A → Set _```

# Commutative monoid property

Consider the following definition of the commutative monoid proposition:

```
record IsCommutativeMonoid′ {A : Set} (_∙_ : A → A → A) (ε : A) : Set where
field
isMonoid : IsMonoid _∙_ ε
comm     : Commutative _∙_```

This definition is correct, but redundant because commutativity and left identity properties entail the right identity property.

A non-redundant and still easy-to-use definition is the following:

```
record IsCommutativeMonoid {A : Set} (_∙_ : A → A → A) (ε : A) : Set where
field
isSemigroup : IsSemigroup _∙_
identityˡ   : LeftIdentity ε _∙_
comm        : Commutative _∙_

open IsSemigroup isSemigroup public

identity : Identity ε _∙_
identity = (identityˡ , identityʳ)
where
open EqR (setoid A)

identityʳ : RightIdentity ε _∙_
identityʳ = λ x → begin
(x ∙ ε)  ≈⟨ comm x ε ⟩
(ε ∙ x)  ≈⟨ identityˡ x ⟩
x        ∎

isMonoid : IsMonoid _∙_ ε
isMonoid = record
{ isSemigroup = isSemigroup
; identity    = identity
}```

• When constructing `IsCommutativeMonoid`, we should provide the semigroup, left identity and commutativity properties.
• When using `IsCommutativeMonoid`, we have semigroup, associativity, monoid, identity and commutativity properties.

# Exercises

1. Define the group property!

2. Define the abelian group property!

# The type of all semigroups

We can define the type of semigroups as

```
record Semigroup : Set₁ where
infixl 7 _∙_
field
Carrier     : Set
_∙_         : Op₂ Carrier
isSemigroup : IsSemigroup _∙_

open IsSemigroup isSemigroup public```

# Exercises

1. Prove that (ℕ, +) is a semigroup (by proving that there is a corresponding element of `Semigroup`)!

2. Define the types of all monoids as a record with fields `Carrier`, `_∙_`, `ε` and `isMonoid`!

# Some defined operations

We can define the multiplication by a natural number in any monoid:

```
module MonoidOperations (m : Monoid) where

open Monoid m

infixr 7 _×′_

_×′_ : ℕ → Carrier → Carrier
0     ×′ x = ε
suc n ×′ x = x ∙ (n ×′ x)```

# Standard Library definitions

You can find the given definitions in the following Standard Library modules:

```
import Algebra.FunctionProperties using (Op₁; Op₂)
import Algebra.FunctionProperties using (Associative; Commutative; LeftIdentity; RightIdentity; Identity) -- and more function properties
import Algebra.Structures using (IsSemigroup; IsMonoid; IsCommutativeMonoid) -- and more
import Algebra using (Semigroup; Monoid; CommutativeMonoid) -- and more
import Algebra.Operations -- some defined operations

import Data.Nat.Properties using (isCommutativeSemiring) -- this contains definitions like ℕ+0-isMonoid```

Notable differences

• The definitions are generalized from `_≡_` to an arbitrary equivalence relation.
• The definitions are universe polymorphic (see later).

Example usage

```
module StdLibUsage where
open import Algebra.Structures as A using (IsCommutativeMonoid)
open import Data.Nat.Properties using (isCommutativeSemiring)

open A.IsCommutativeSemiring
open A.IsCommutativeMonoid (+-isCommutativeMonoid isCommutativeSemiring)

ex : ∀ n → (n + 1) + 1 ≡ n + 2
ex n = assoc n 1 1```