We start by defining operations and laws these operations obey.

```
open import Types.equality
open import Types.functions
open import Types.product
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
module Types.operations {a ℓ} {A : Set a} (_==_ : Rel A ℓ) where
```

A binary operation $ ★ $ on a set A is a function (function type!) that takes two elements of type A and returns an element of A:

`★ : A × A → A`

More often the operation is applied to the two objects `x, y ∈ A`

as $ x ★ y $.

A unary operation on the other hand operates on only one element of A to return an element of A:

`♠ : A → A`

In agda, a homogenous binary operation `★ A`

can be defined as:

and a unary operation as:

We now write a few laws that operators could follow. Essentially, structures built on top of these operators would end up following the same laws as the underlying operator. We have already seen some of these laws in laws of boolean algebra, these are universe polymorphism-accounted general versions of those laws.

Mathematically, given an operation `★`

, it is called associative if:

```
∀ x, y, z ∈ A,
operation ★ is associative if:
x ★ (y ★ z) ≡ (x ★ y) ★ z
```

Commutativity is defined as:

```
∀ x, y ∈ A,
operation ★ is commutative if:
x ★ y ≡ y ★ x
```

```
∀ x ∈ A,
if id is the identity object of A,
x ★ id ≡ x
id ★ x ≡ x
```

We treat identity as a pair of right and left identities. This helps in working with non-commutative types as well.

```
LeftIdentity : A → ★ A → Set _
LeftIdentity e _∙_ = ∀ x → (e ∙ x) == x
RightIdentity : A → ★ A → Set _
RightIdentity e _∙_ = ∀ x → (x ∙ e) == x
Identity : A → ★ A → Set _
Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙
```

```
∀ x ∈ A,
x ★ 0 ≡ 0
0 ★ x ≡ 0
```

How does our object interact with `0`

? We define that here.

```
LeftZero : A → ★ A → Set _
LeftZero z _∙_ = ∀ x → (z ∙ x) == z
RightZero : A → ★ A → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) == z
Zero : A → ★ A → Set _
Zero z ∙ = LeftZero z ∙ × RightZero z ∙
```

```
∀ x ∈ A, ∃ x⁻¹ ∈ A such that
x ★ x⁻¹ ≡ id
x⁻¹ ★ x ≡ id
```

Given any unary function `_⁻¹`

, we define what it takes for the function to qualify as an inverse.

```
LeftInverse : A → ♠ A → ★ A → Set _
LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) == e
RightInverse : A → ♠ A → ★ A → Set _
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) == e
Inverse : A → ♠ A → ★ A → Set _
Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙
```

```
∀ x, y, z ∈ A,
operation ★ is distributive if:
( x ★ y ) ★ z ≡ x ★ y × y ★ z
```

```
_DistributesOverˡ_ : ★ A → ★ A → Set _
_*_ DistributesOverˡ _+_ =
∀ x y z → (x * (y + z)) == ((x * y) + (x * z))
_DistributesOverʳ_ : ★ A → ★ A → Set _
_*_ DistributesOverʳ _+_ =
∀ x y z → ((y + z) * x) == ((y * x) + (z * x))
_DistributesOver_ : ★ A → ★ A → Set _
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
```

```
∀ x ∈ A and two operations
∙ : A → A → A
∘ : A → A → A
operation ∙ absorbs ∘ if:
x ∙ (x ∘ y) ≡ x
and ∘ absorbs ∙ if:
x ∘ (x ∙ y) ≡ x
and if both are satisfied collectively ∙ and ∘ are absorptive.
```

```
_Absorbs_ : ★ A → ★ A → Set _
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) == x
Absorptive : ★ A → ★ A → Set _
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
```

```
∀ x, y ∈ A
and a function • : A → A → A,
(x • y) == (x • z) ⟹ y == z
```

```
LeftCancellative : ★ A → Set _
LeftCancellative _•_ = ∀ x {y z} → (x • y) == (x • z) → y == z
RightCancellative : ★ A → Set _
RightCancellative _•_ = ∀ {x} y z → (y • x) == (z • x) → y == z
Cancellative : ★ A → Set _
Cancellative _•_ = LeftCancellative _•_ × RightCancellative _•_
```

```
Given
a₁, a₂ ∈ A
b₁ b₂ ∈ B
∙ : A → B,
if a₁ ≡ a₂,
b₁ = ∙ a₁
b₂ = ∙ a₂
then b₁ ≡ b₂
```

A congruent relation preserves equivalences:

- for binary relation
`♣`

, if $ (x₁, y₁) == (x₂, y₂) $ then $ (x₁ ♣ y₁) == (x₂ ♣ y₂) $. - for unary relation
`♡`

, if $ x == y $ then $ ♡ x == ♡ y $.

```
Congruent₁ : ♠ A → Set _
Congruent₁ f = f Preserves _==_ ⟶ _==_
Congruent₂ : ★ A → Set _
Congruent₂ ∙ = ∙ Preserves₂ _==_ ⟶ _==_ ⟶ _==_
LeftCongruent : ★ A → Set _
LeftCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _==_ ⟶ _==_
RightCongruent : ★ A → Set _
RightCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _==_ ⟶ _==_
```

We finally define what we mean by a functions “respects” an operation or is invariant of it. For a function $ f $ and an operation $ ∘ $, if $ x ∘ y ⟹ f(x) ∘ f(y) $, we say the function $ f $ respects the operation $ ∘ $. We define two versions of this utility here

`_Respects_`

for already commutative laws`_Respects₂_`

which combines left`_Respectsˡ_`

and right`_Respectsʳ_`

laws

```
_Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
→ (A → Set ℓ₁)
→ Rel A ℓ₂
→ Set _
P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y
_Respectsʳ_ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
→ Rel A ℓ₁
→ Rel A ℓ₂
→ Set _
P Respectsʳ _∼_ = ∀ {x} → (P x) Respects _∼_
_Respectsˡ_ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
→ Rel A ℓ₁
→ Rel A ℓ₂
→ Set _
P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_
_Respects₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a}
→ Rel A ℓ₁
→ Rel A ℓ₂
→ Set _
P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)
```