Contents Previous Next


Operations

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:

_ :  {a}  Set a  Set a
  ★ A = A  A  A

and a unary operation as:

_ :  {a}  Set a  Set a
  ♠ A = A  A

Operator laws

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.

Associativity

Figure 1: Associative

Mathematically, given an operation , it is called associative if:

∀ x, y, z ∈ A,
operation ★ is associative if:

x ★ (y ★ z) ≡ (x ★ y) ★ z
  Associative : ★ A  Set _
  Associative __ =  x y z  ((x ∙ y) ∙ z) == (x ∙ (y ∙ z))

Commutativity

Figure 2: Commutative

Commutativity is defined as:

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

x ★ y ≡ y ★ x
  Commutative : ★ A  Set _
  Commutative __ =  x y  (x ∙ y) == (y ∙ x)

Identity

Figure 3: Identity
∀ 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 ∙

Elimination

Figure 4: Elimination
∀ 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 ∙

Inverse

Figure 5: Inverse
∀ 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 ⁻¹ ∙

Distributive

Figure 6: Distributive
∀ 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ʳ +)

Absorptive

Figure 7: Absorption
∀ 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 ∙)

Cancellative

Figure 8: Cancellation
∀ 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 __

Congruence

Figure 9: Congruence
Given
  a₁, a₂ ∈ A
  b₁ b₂ ∈ B
  ∙ : A → B,

if a₁ ≡ a₂,
   b₁ = ∙ a₁
   b₂ = ∙ a₂
then b₁ ≡ b₂

A congruent relation preserves equivalences:

  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 _==__==_

Respecting an relation

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_ :  {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ˡ __)

Equational Reasoning