- Equalities
- Definitional Equality
- Computational Equality
- Propositional Equality
- Relations, with universe polymorphism
- Setoids

```
module Types.equality where
open import Lang.dataStructures using (
Bool; true; false;
⟂; ⊤; ℕ; List;
one; two; three; four; five; six; seven; eight; nine; ten; zero; succ; _+_;
_::_; [])
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.functions using (_on_; flip)
```

Equality is perhaps one of the most richest but most naively understood concepts. Here we try to provide some structural analysis as to what equality really means in various contexts of mathematics. Equality is treated as a relation in type theory and can be classified broadly as of three kinds:

- Propositional equality
- Computational equality
- Definitional equality

Definitional equality is the most basic notion of equality which appeals to our notion of equality being the sameness of meaning (by definition). For example, `9`

and `3 + 3`

represent the same thing and hence are definitionally equal `9 ≡ 3²`

. Similarly `two ≡ succ (succ zero)`

.

Here, `defEqual₁`

and `defEqual₂`

both are equal, with equality of the kind “definitional equality”.

This kind of equality describes the sameness of types that are not directly equal but can be reduced to be equal. “Reduction” here implies mathematical reduction, referring to rewriting expressions into simpler forms. An example of such an equality is applying a function \[(λ x.x+x)(2) ≡ 2 + 2\] Expansions of recursors also falls under this kind of equality: \[2 + 2 ≡ succ (succ zero) + succ (succ zero) ≡ succ (succ (succ (succ zero)))\] Practically, computational equality is included into definitional equality and is also known as “Judgemental equality”.

Definitional and computational equalities describe something intrinsic - a property that does not depend upon a proof. For example, `a + b ≡ b + a`

cannot be proven to be definitionally equal unless the concrete values of `a`

and `b`

are known. However, if they’re natural numbers `a, b ∈ ℕ`

, then the statement `a + b ≡ b + a`

requires a proof to claim its truthfulness. Given `a, b ∈ ℕ`

, we can prove that `a + b ≡ b + a`

or in other words that there exists an identity of type `Id : a + b ≡ b + a`

where `Id`

is a proposition − exhibiting a term belonging to such a type is exhibiting (i.e. proving) such a propositional equality.

However, other notions of equalities can be defined that do require proofs. Consider for example natural language - when we say “all flowers are beautiful” the “all flowers” part of the sentence implies all flowers are equal in some way. Or, consider natural numbers `a + b = b + a ∀ a, b ∈ ℕ`

. Here we would need to prove the symmetry of the `+`

operator in order to prove the equality. Such equalities that require to be specified come under the umbrella of propositional equality. Propositional equality is a kind of equality which requires a proof, and hence the equality itself is also a type `∼`

:

Reflexivity is defined with the definition of `∼`

by the keyword `same`

, the others being:

Symmetry is the property where binary a relation’s behavior does not depend upon its argument’s position (left or right):

Transitivity is when a binary relation `_∼_`

and \(x ∼ y and y ∼ z ⟹ x ∼ z\)

Functions that when applied to objects of a type, do not alter the operation of equality can be defined as:

If `a = b`

and if `predicate a = true`

⟹ `predicate b = true`

```
substitution : ∀ {A : Set} {x y : A} (Predicate : A → Set)
→ x ∼ y
→ Predicate x
→ Predicate y
substitution Predicate same p = p
```

Any relation which satisfies the above properties of `reflexivity`

, `transitivity`

and `symmetry`

can be considered an equivalence relation and hence can judge a propositional equality.

We now present a more formal machinery for relations. We use universe polymorphism throughout to develop this machinery.

We first re-define propositional equality within the framework of universe polymorphism:

Nullary relations are functions that can take any object and return an empty set `∅`

:

In logic, a predicate can essentially be defined as a function that returns a binary value - whether the proposition that the predicate represents is true or false. In type theory, however, we define predicate in a different way. A predicate for us is a function that exists (and hence, is true):

The empty (or false) predicate becomes:

The singleton predicate (constructor):

A heterogeneous binary relation is defined as:

and a homogenous one as:

In type theory, an implication $ A ⟹ B $ is just a function type $ f: A → B $, and if `f`

exists, the implication does too. We define implication between two relations in agda as:

```
_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ REL A B ℓ₁
→ REL A B ℓ₂
→ Set _
P ⇒ Q = ∀ {i j} → P i j → Q i j
```

A function `f : A → B`

is invariant to two homogenous relations `Rel A ℓ₁`

and `Rel B ℓ₂`

if $ ∀ x, y ∈ A _{and} f(x), f(y) ∈ B, f(Rel x y) ⟹ (Rel f(x) f(y)) $:

```
_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ Rel A ℓ₁
→ (A → B)
→ Rel B ℓ₂
→ Set _
P =[ f ]⇒ Q = P ⇒ (Q on f)
```

A function `f`

preserves an underlying relation while operating on a datatype if:

```
_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ (A → B)
→ Rel A ℓ₁
→ Rel B ℓ₂
→ Set _
f Preserves P ⟶ Q = P =[ f ]⇒ Q
```

Similarly, a binary operation `_+_`

preserves the underlying relation if:

```
_Preserves₂_⟶_⟶_ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
→ (A → B → C)
→ Rel A ℓ₁
→ Rel B ℓ₂
→ Rel C ℓ₃
→ Set _
_+_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)
```

Properties of binary relations:

```
Sym : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ REL A B ℓ₁
→ REL B A ℓ₂
→ Set _
Sym P Q = P ⇒ flip Q
Symmetric : ∀ {a ℓ} {A : Set a}
→ Rel A ℓ
→ Set _
Symmetric _∼_ = Sym _∼_ _∼_
```

```
Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
→ REL A B ℓ₁
→ REL B C ℓ₂
→ REL A C ℓ₃
→ Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
Transitive : ∀ {a ℓ} {A : Set a}
→ Rel A ℓ
→ Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_
```

Finally, we define an equivalence relation for binary relations:

```
record IsEquivalence {a ℓ} {A : Set a}
(_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
field
rfl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_
reflexive : _≡_ ⇒ _≈_
reflexive refl = rfl
```

We use the new structures to re-define the properties of propositional equality.

```
module ≡-properties {a} {A : Set a} where
sym-≡ : Symmetric {A = A} _≡_
sym-≡ refl = refl
trans-≡ : Transitive {A = A} _≡_
trans-≡ refl p = p
isEquivalence : IsEquivalence {A = A} _≡_
isEquivalence = record
{ rfl = refl
; sym = sym-≡
; trans = trans-≡
}
cong-≡ : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y : A}
→ x ≡ y
→ f x ≡ f y
cong-≡ f refl = refl
subs-≡ : ∀ {a} {A : Set a}{x y : A} (Predicate : A → Set)
→ x ≡ y
→ Predicate x
→ Predicate y
subs-≡ Predicate refl p = p
```

Equality, or specifically, equivalence is at the heart of mathematics. In order to build more complex structures, we introduce a new datatype, which essentially encapsulates any datatype and it’s equivalence operation:

```
record Setoid c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix 4 _≈_
field
Data : Set c
_≈_ : Rel Data ℓ
isEquivalence : IsEquivalence _≈_
open IsEquivalence isEquivalence public
```