---
title : "Equality: Equality and equational reasoning"
permalink : /Equality/
---
```agda
module plfa.part1.Equality where
```
Much of our reasoning has involved equality. Given two terms `M`
and `N`, both of type `A`, we write `M ≡ N` to assert that `M` and `N`
are interchangeable. So far we have treated equality as a primitive,
here we show how to define it as an inductive datatype.
## Imports
This chapter has no imports. Every chapter in this book, and nearly
every module in the Agda standard library, imports equality.
Since we define equality here, any import would create a conflict.
## Equality
We declare equality as follows:
```agda
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
```
In other words, for any type `A` and for any `x` of type `A`, the
constructor `refl` provides evidence that `x ≡ x`. Hence, every value
is equal to itself, and we have no other way of showing values
equal. The definition features an asymmetry, in that the
first argument to `_≡_` is given by the parameter `x : A`, while the
second is given by an index in `A → Set`. This follows our policy
of using parameters wherever possible. The first argument to `_≡_`
can be a parameter because it doesn't vary, while the second must be
an index, so it can be required to be equal to the first.
We declare the precedence of equality as follows:
```agda
infix 4 _≡_
```
We set the precedence of `_≡_` at level 4, the same as `_≤_`,
which means it binds less tightly than any arithmetic operator.
It associates neither to left nor right; writing `x ≡ y ≡ z`
is illegal.
## Equality is an equivalence relation
An equivalence relation is one which is reflexive, symmetric, and transitive.
Reflexivity is built-in to the definition of equality, via the
constructor `refl`. It is straightforward to show symmetry:
```agda
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym refl = refl
```
How does this proof work? The argument to `sym` has type `x ≡ y`, but
on the left-hand side of the equation the argument has been
instantiated to the pattern `refl`, which requires that `x` and `y`
are the same. Hence, for the right-hand side of the equation we need
a term of type `x ≡ x`, and `refl` will do.
It is instructive to develop `sym` interactively. To start, we supply
a variable for the argument on the left, and a hole for the body on
the right:
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym e = {! !}
If we go into the hole and type `C-c C-,` then Agda reports:
Goal: .y ≡ .x
————————————————————————————————————————————————————————————
e : .x ≡ .y
.y : .A
.x : .A
.A : Set
If in the hole we type `C-c C-c e` then Agda will instantiate `e` to
all possible constructors, with one equation for each. There is only
one possible constructor:
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym refl = {! !}
If we go into the hole again and type `C-c C-,` then Agda now reports:
Goal: .x ≡ .x
————————————————————————————————————————————————————————————
.x : .A
.A : Set
This is the key step---Agda has worked out that `x` and `y` must be
the same to match the pattern `refl`!
Finally, if we go back into the hole and type `C-c C-r` it will
instantiate the hole with the one constructor that yields a value of
the expected type:
sym : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ y ≡ x
sym refl = refl
This completes the definition as given above.
Transitivity is equally straightforward:
```agda
trans : ∀ {A : Set} {x y z : A}
→ x ≡ y
→ y ≡ z
-----
→ x ≡ z
trans refl refl = refl
```
Again, a useful exercise is to carry out an interactive development,
checking how Agda's knowledge changes as each of the two arguments is
instantiated.
## Congruence and substitution {#cong}
Equality satisfies _congruence_. If two terms are equal,
they remain so after the same function is applied to both:
```agda
cong : ∀ {A B : Set} (f : A → B) {x y : A}
→ x ≡ y
---------
→ f x ≡ f y
cong f refl = refl
```
Congruence of functions with two arguments is similar:
```agda
cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
→ u ≡ x
→ v ≡ y
-------------
→ f u v ≡ f x y
cong₂ f refl refl = refl
```
Equality is also a congruence in the function position of an application.
If two functions are equal, then applying them to the same term
yields equal terms:
```agda
cong-app : ∀ {A B : Set} {f g : A → B}
→ f ≡ g
---------------------
→ ∀ (x : A) → f x ≡ g x
cong-app refl x = refl
```
Equality also satisfies _substitution_.
If two values are equal and a predicate holds of the first then it also holds of the second:
```agda
subst : ∀ {A : Set} {x y : A} (P : A → Set)
→ x ≡ y
---------
→ P x → P y
subst P refl px = px
```
A predicate is a proposition over values of some type `A`, and since we model
_propositions as types_, a predicate is a type parameterized in `A`.
As an example, `even : ℕ → Set` and `odd : ℕ → Set` from
Chapter [Relations](/Relations/#even-and-odd) are predicates on natural numbers `ℕ`.
(We will compare representing predicates as data types `A → Set`
versus functions to booleans `A → Bool` in Chapter [Decidable](/Decidable/).)
## Chains of equations
Here we show how to support reasoning with chains of equations, as
used throughout the book. We package the declarations into a module,
named `≡-Reasoning`, to match the format used in Agda's standard
library:
```agda
module ≡-Reasoning {A : Set} where
infix 1 begin_
infixr 2 step-≡-∣ step-≡-⟩
infix 3 _∎
begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
begin x≡y = x≡y
step-≡-∣ : ∀ (x : A) {y : A} → x ≡ y → x ≡ y
step-≡-∣ x x≡y = x≡y
step-≡-⟩ : ∀ (x : A) {y z : A} → y ≡ z → x ≡ y → x ≡ z
step-≡-⟩ x y≡z x≡y = trans x≡y y≡z
syntax step-≡-∣ x x≡y = x ≡⟨⟩ x≡y
syntax step-≡-⟩ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
_∎ : ∀ (x : A) → x ≡ x
x ∎ = refl
open ≡-Reasoning
```
This is our first use of a nested module. It consists of the keyword
`module` followed by the module name and any parameters, explicit or
implicit, and the keyword `where`; this is followed by the contents of
the module, which must be indented. Modules may contain any sort of
declaration, including other nested modules. Nested modules are
similar to the top-level modules that constitute each chapter of this
book, save that the body of a top-level module need not be indented.
Opening the module makes all of the definitions available in the
current environment.
This is also our first use of a syntax declaration, which specifies
that the term on the left may be written with the syntax on the right.
The syntax `x ≡⟨ x≡y ⟩ y≡z` inherits the fixity `infixr 2` declared
for `step-≡-⟩`, and the special syntax is available when the identifier
`step-≡-⟩` is imported. Similarly for `step-≡-∣`.
Rather than introducing `step-≡` with special syntax, we might have
declared `_≡⟨_⟩′_` directly:
```agda
_≡⟨_⟩′_ : ∀ {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩′ y≡z = trans x≡y y≡z
```
The reason for indirection is that `step-≡-⟩` reverses
the order of the arguments, which happens to allow Agda to
perform type inference more efficiently. We will encounter some
long chains in Chapter [Lambda](/Lambda/), so efficiency can be
important.
Let's look at a proof of transitivity
as a chain of equations:
```agda
trans′ : ∀ {A : Set} {x y z : A}
→ x ≡ y
→ y ≡ z
-----
→ x ≡ z
trans′ {A} {x} {y} {z} x≡y y≡z =
begin
x
≡⟨ x≡y ⟩
y
≡⟨ y≡z ⟩
z
∎
```
According to the fixity declarations, the body parses as follows:
begin (x ≡⟨ x≡y ⟩ (y ≡⟨ y≡z ⟩ (z ∎)))
The application of `begin` is purely cosmetic, as it simply returns
its argument. That argument consists of `_≡⟨_⟩_` applied to `x`,
`x≡y`, and `y ≡⟨ y≡z ⟩ (z ∎)`. The first argument is a term, `x`,
while the second and third arguments are proofs of `x ≡ y` and `y ≡ z`
respectively, which are combined by `trans` in the body of `_≡⟨_⟩_` to
yield a proof of `x ≡ z`. The proof of `y ≡ z` consists of `_≡⟨_⟩_`
applied to `y`, `y≡z`, and `z ∎`. The first argument is a term, `y`,
while the second and third arguments are proofs of `y ≡ z` and `z ≡ z`
respectively, which are combined by `trans` in the body of `_≡⟨_⟩_` to
yield a proof of `y ≡ z`. Finally, the proof of `z ≡ z` consists of
`_∎` applied to the term `z`, which yields `refl`. After
simplification, the body is equivalent to the term:
trans x≡y (trans y≡z refl)
We could replace any use of a chain of equations by a chain of
applications of `trans`; the result would be more compact but harder
to read. The trick behind `∎` means that a chain of equalities
simplifies to a chain of applications of `trans` that ends in `trans e
refl`, where `e` is a term that proves some equality.
(That trick might seem inefficient, since `trans e refl` and `e` both
prove the same equality. But that inefficiency is key to our nice
notation for chains of equalities. One shouldn't fear inefficiency
if it improves readability!)
#### Exercise `trans` and `≡-Reasoning` (practice)
Sadly, we cannot use the definition of `trans′` using `≡-Reasoning` as the
definition for `trans`. Can you see why? (Hint: look at the definition
of `_≡⟨_⟩_`)
```agda
-- Your code goes here
-- because `_≡⟨_⟩_` uses trans
```
## Chains of equations, another example
As a second example of chains of equations, we repeat the proof that addition
is commutative. We first repeat the definitions of naturals and addition.
We cannot import them because (as noted at the beginning of this chapter)
it would cause a conflict:
```agda
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)
```
To save space we postulate (rather than prove in full) two lemmas:
```agda
postulate
+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
```
This is our first use of a _postulate_. A postulate specifies a
signature for an identifier but no definition. Here we postulate
something proved earlier to save space. Postulates must be used with
caution. If we postulate something false then we could use Agda to
prove anything whatsoever.
We then repeat the proof of commutativity:
```agda
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
begin
m + zero
≡⟨ +-identity m ⟩
m
≡⟨⟩
zero + m
∎
+-comm m (suc n) =
begin
m + suc n
≡⟨ +-suc m n ⟩
suc (m + n)
≡⟨ cong suc (+-comm m n) ⟩
suc (n + m)
≡⟨⟩
suc n + m
∎
```
The reasoning here is similar to that in the
preceding section. We use
`_≡⟨⟩_` when no justification is required.
One can think of `_≡⟨⟩_` as equivalent to `_≡⟨ refl ⟩_`.
Agda always treats a term as equivalent to its
simplified term. The reason that one can write
suc (n + m)
≡⟨⟩
suc n + m
is because Agda treats both terms as the same.
This also means that one could instead interchange
the lines and write
suc n + m
≡⟨⟩
suc (n + m)
and Agda would not object. Agda only checks that the terms separated
by `≡⟨⟩` have the same simplified form; it's up to us to write them in
an order that will make sense to the reader.
#### Exercise `≤-Reasoning` (stretch)
The proof of monotonicity from
Chapter [Relations](/Relations/)
can be written in a more readable form by using an analogue of our
notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use
it to write out an alternative proof that addition is monotonic with
regard to inequality. Rewrite all of `+-monoˡ-≤`, `+-monoʳ-≤`, and `++-mono-≤-mono-≤`.
```agda
-- Your code goes here
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n : ℕ}
--------
→ zero ≤ n
s≤s : ∀ {m n : ℕ}
→ m ≤ n
-------------
→ suc m ≤ suc n
infix 4 _≤_
≤-trans : ∀ {m n p : ℕ}
→ m ≤ n
→ n ≤ p
-----
→ m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)
≤-≡-trans : ∀ {m n p : ℕ}
→ m ≡ n
→ n ≤ p
-----
→ m ≤ p
≤-≡-trans refl z≤n = z≤n
≤-≡-trans refl (s≤s n≤p) = s≤s (≤-≡-trans refl n≤p)
module ≤-Reasoning where
infix 1 begin'_
infixr 2 step-≤-∣ step-≤-⟩ step-≤-≡-⟩
infix 3 _∎'
begin'_ : ∀ {x y : ℕ} → x ≤ y → x ≤ y
begin' x≤y = x≤y
step-≤-∣ : ∀ (x : ℕ) {y : ℕ} → x ≤ y → x ≤ y
step-≤-∣ x x≤y = x≤y
step-≤-⟩ : ∀ (x : ℕ) {y z : ℕ} → y ≤ z → x ≤ y → x ≤ z
step-≤-⟩ x y≤z x≤y = ≤-trans x≤y y≤z
step-≤-≡-⟩ : ∀ (x : ℕ) {y z : ℕ} → y ≤ z → x ≡ y → x ≤ z
step-≤-≡-⟩ x y≤z x≡y = ≤-≡-trans x≡y y≤z
syntax step-≤-∣ x x≤y = x ≤⟨⟩ x≤y
syntax step-≤-⟩ x y≤z x≤y = x ≤⟨ x≤y ⟩ y≤z
syntax step-≤-≡-⟩ x y≤z x≡y = x ≡'⟨ x≡y ⟩ y≤z
_∎' : ∀ (x : ℕ) → x ≤ x
zero ∎' = z≤n
suc x ∎' = s≤s (x ∎')
open ≤-Reasoning
+-monoˡ-≤ : (x y z : ℕ) → x ≤ y → x + z ≤ y + z
+-monoˡ-≤ x y zero x≤y =
begin'
x + zero
≡'⟨ +-identity x ⟩
x
≤⟨ x≤y ⟩
y
≡'⟨ sym (+-identity y) ⟩
y + zero
∎'
+-monoˡ-≤ x y (suc z) x≤y =
begin'
x + (suc z)
≡'⟨ +-comm x (suc z) ⟩
(suc z) + x
≡'⟨ refl ⟩
suc (z + x)
≡'⟨ cong suc (+-comm z x) ⟩
suc (x + z)
≤⟨ s≤s (+-monoˡ-≤ x y z x≤y) ⟩
suc (y + z)
≡'⟨ cong suc (+-comm y z) ⟩
suc (z + y)
≡'⟨ refl ⟩
(suc z) + y
≡'⟨ +-comm (suc z) y ⟩
y + (suc z)
∎'
+-monoʳ-≤ : (x y z : ℕ) → x ≤ y → z + x ≤ z + y
+-monoʳ-≤ x y zero x≤y = x≤y
+-monoʳ-≤ x y (suc z) x≤y =
begin'
suc (z + x)
≤⟨ s≤s (+-monoʳ-≤ x y z x≤y) ⟩
suc (z + y)
∎'
+-mono-≤ : ∀ (w x y z : ℕ) → w ≤ x → y ≤ z → w + y ≤ x + z
+-mono-≤ w x y z w≤x y≤z = ≤-trans (+-monoˡ-≤ w x y w≤x) (+-monoʳ-≤ y z x y≤z)
```
## Rewriting
Consider a property of natural numbers, such as being even.
We repeat the earlier definition:
```agda
data even : ℕ → Set
data odd : ℕ → Set
data even where
even-zero : even zero
even-suc : ∀ {n : ℕ}
→ odd n
------------
→ even (suc n)
data odd where
odd-suc : ∀ {n : ℕ}
→ even n
-----------
→ odd (suc n)
```
In the previous section, we proved addition is commutative. Given
evidence that `even (m + n)` holds, we ought also to be able to take
that as evidence that `even (n + m)` holds.
Agda includes special notation to support just this kind of reasoning,
the `rewrite` notation we encountered earlier.
To enable this notation, we use pragmas to tell Agda which type
corresponds to equality:
```agda
{-# BUILTIN EQUALITY _≡_ #-}
```
We can then prove the desired property as follows:
```agda
even-comm : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm m n ev rewrite +-comm n m = ev
```
Here `ev` ranges over evidence that `even (m + n)` holds, and we show
that it also provides evidence that `even (n + m)` holds. In
general, the keyword `rewrite` is followed by evidence of an
equality, and that equality is used to rewrite the type of the
goal and of any variable in scope.
It is instructive to develop `even-comm` interactively. To start, we
supply variables for the arguments on the left, and a hole for the
body on the right:
even-comm : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm m n ev = {! !}
If we go into the hole and type `C-c C-,` then Agda reports:
Goal: even (n + m)
————————————————————————————————————————————————————————————
ev : even (m + n)
n : ℕ
m : ℕ
Now we add the rewrite:
even-comm : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm m n ev rewrite +-comm n m = {! !}
If we go into the hole again and type `C-c C-,` then Agda now reports:
Goal: even (m + n)
————————————————————————————————————————————————————————————
ev : even (m + n)
n : ℕ
m : ℕ
The arguments have been swapped in the goal. Now it is trivial to see
that `ev` satisfies the goal, and typing `C-c C-a` in the hole causes
it to be filled with `ev`. The command `C-c C-a` performs an
automated search, including checking whether a variable in scope has
the same type as the goal.
## Multiple rewrites
One may perform multiple rewrites, each separated by a vertical bar. For instance,
here is a second proof that addition is commutative, relying on rewrites rather
than chains of equalities:
```agda
+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ zero n rewrite +-identity n = refl
+-comm′ (suc m) n rewrite +-suc n m | +-comm′ m n = refl
```
This is far more compact. Among other things, whereas the previous
proof required `cong suc (+-comm m n)` as the justification to invoke
the inductive hypothesis, here it is sufficient to rewrite with
`+-comm m n`, as rewriting automatically takes congruence into
account. Although proofs with rewriting are shorter, proofs as chains
of equalities are easier to follow, and we will stick with the latter
when feasible.
## Rewriting expanded
The `rewrite` notation is in fact shorthand for an appropriate use of `with`
abstraction:
```agda
even-comm′ : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm′ m n ev with m + n | +-comm m n
... | .(n + m) | refl = ev
```
In general, one can follow `with` by any number of expressions,
separated by bars, where each following equation has the same number
of patterns. We often write expressions and the corresponding
patterns so they line up in columns, as above. Here the first column
asserts that `m + n` and `n + m` are identical, and the second column
justifies that assertion with evidence of the appropriate equality.
Note also the use of the _dot pattern_, `.(n + m)`. A dot pattern
consists of a dot followed by an expression, and is used when other
information forces the value matched to be equal to the value of the
expression in the dot pattern. In this case, the identification of
`m + n` and `n + m` is justified by the subsequent matching of
`+-comm m n` against `refl`. One might think that the first clause is
redundant as the information is inherent in the second clause, but in
fact Agda is rather picky on this point: omitting the first clause or
reversing the order of the clauses will cause Agda to report an error.
(Try it and see!)
In this case, we can avoid rewrite by simply applying the substitution
function defined earlier:
```agda
even-comm″ : ∀ (m n : ℕ)
→ even (m + n)
------------
→ even (n + m)
even-comm″ m n = subst even (+-comm m n)
```
Nonetheless, rewrite is a vital part of the Agda toolkit. We will use
it sparingly, but it is occasionally essential.
## Leibniz equality
The form of asserting equality that we have used is due to Martin-Löf,
and was published in 1975. An older form is due to Leibniz, and
was published in 1686. Leibniz asserted the _identity of
indiscernibles_: two objects are equal if and only if they satisfy the
same properties. This principle sometimes goes by the name Leibniz'
Law, and is closely related to Spock's Law, "A difference that makes
no difference is no difference". Here we define Leibniz equality,
and show that two terms satisfy Leibniz equality if and only if they
satisfy Martin-Löf equality.
Leibniz equality is usually formalised to state that `x ≐ y` holds if
every property `P` that holds of `x` also holds of `y`. Perhaps
surprisingly, this definition is sufficient to also ensure the
converse, that every property `P` that holds of `y` also holds of `x`.
Let `x` and `y` be objects of type `A`. We say that `x ≐ y` holds if
for every predicate `P` over type `A` we have that `P x` implies `P y`:
```agda
_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y
```
We cannot write the left-hand side of the equation as `x ≐ y`,
and instead we write `_≐_ {A} x y` to provide access to the implicit
parameter `A` which appears on the right-hand side.
This is our first use of _levels_. We cannot assign `Set` the type
`Set`, since this would lead to contradictions such as Russell's
Paradox and Girard's Paradox. Instead, there is a hierarchy of types,
where `Set : Set₁`, `Set₁ : Set₂`, and so on. In fact, `Set` itself
is just an abbreviation for `Set₀`. Since the equation defining `_≐_`
mentions `Set` on the right-hand side, the corresponding signature
must use `Set₁`. We say a bit more about levels below.
Leibniz equality is reflexive and transitive,
where the first follows by a variant of the identity function
and the second by a variant of function composition:
```agda
refl-≐ : ∀ {A : Set} {x : A}
→ x ≐ x
refl-≐ P Px = Px
trans-≐ : ∀ {A : Set} {x y z : A}
→ x ≐ y
→ y ≐ z
-----
→ x ≐ z
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)
```
Symmetry is less obvious. We have to show that if `P x` implies `P y`
for all predicates `P`, then the implication holds the other way round
as well:
```agda
sym-≐ : ∀ {A : Set} {x y : A}
→ x ≐ y
-----
→ y ≐ x
sym-≐ {A} {x} {y} x≐y P = Qy
where
Q : A → Set
Q z = P z → P x
Qx : Q x
Qx = refl-≐ P
Qy : Q y
Qy = x≐y Q Qx
```
Given `x ≐ y`, a specific `P`, we have to construct a proof that `P y`
implies `P x`. To do so, we instantiate the equality with a predicate
`Q` such that `Q z` holds if `P z` implies `P x`. The property `Q x`
is trivial by reflexivity, and hence `Q y` follows from `x ≐ y`. But
`Q y` is exactly a proof of what we require, that `P y` implies `P x`.
We now show that Martin-Löf equality implies
Leibniz equality, and vice versa. In the forward direction, if we know
`x ≡ y` we need for any `P` to take evidence of `P x` to evidence of `P y`,
which is easy since equality of `x` and `y` implies that any proof
of `P x` is also a proof of `P y`:
```agda
≡-implies-≐ : ∀ {A : Set} {x y : A}
→ x ≡ y
-----
→ x ≐ y
≡-implies-≐ x≡y P = subst P x≡y
```
This direction follows from substitution, which we showed earlier.
In the reverse direction, given that for any `P` we can take a proof of `P x`
to a proof of `P y` we need to show `x ≡ y`:
```agda
≐-implies-≡ : ∀ {A : Set} {x y : A}
→ x ≐ y
-----
→ x ≡ y
≐-implies-≡ {A} {x} {y} x≐y = Qy
where
Q : A → Set
Q z = x ≡ z
Qx : Q x
Qx = refl
Qy : Q y
Qy = x≐y Q Qx
```
The proof is similar to that for symmetry of Leibniz equality. We take
`Q` to be the predicate that holds of `z` if `x ≡ z`. Then `Q x` is
trivial by reflexivity of Martin-Löf equality, and hence `Q y`
follows from `x ≐ y`. But `Q y` is exactly a proof of what we
require, that `x ≡ y`.
(Parts of this section are adapted from *≐≃≡: Leibniz Equality is
Isomorphic to Martin-Löf Identity, Parametrically*, by Andreas Abel,
Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
draft, 2017.)
## Universe polymorphism {#unipoly}
As we have seen, not every type belongs to `Set`, but instead every
type belongs somewhere in the hierarchy `Set₀`, `Set₁`, `Set₂`, and so on,
where `Set` abbreviates `Set₀`, and `Set₀ : Set₁`, `Set₁ : Set₂`, and so on.
The definition of equality given above is fine if we want to compare two
values of a type that belongs to `Set`, but what if we want to compare
two values of a type that belongs to `Set ℓ` for some arbitrary level `ℓ`?
The answer is _universe polymorphism_, where a definition is made
with respect to an arbitrary level `ℓ`. To make use of levels, we
first import the following:
```agda
open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)
```
We rename constructors `zero` and `suc` to `lzero` and `lsuc` to avoid confusion
between levels and naturals.
Levels are isomorphic to natural numbers, and have similar constructors:
lzero : Level
lsuc : Level → Level
The names `Set₀`, `Set₁`, `Set₂`, and so on, are abbreviations for
Set lzero
Set (lsuc lzero)
Set (lsuc (lsuc lzero))
and so on. There is also an operator
_⊔_ : Level → Level → Level
that given two levels returns the larger of the two.
Here is the definition of equality, generalised to an arbitrary level:
```agda
data _≡′_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
refl′ : x ≡′ x
```
Similarly, here is the generalised definition of symmetry:
```agda
sym′ : ∀ {ℓ : Level} {A : Set ℓ} {x y : A}
→ x ≡′ y
------
→ y ≡′ x
sym′ refl′ = refl′
```
For simplicity, we avoid universe polymorphism in the definitions given in
the text, but most definitions in the standard library, including those for
equality, are generalised to arbitrary levels as above.
Here is the generalised definition of Leibniz equality:
```agda
_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y
```
Before the signature used `Set₁` as the type of a term that includes
`Set`, whereas here the signature uses `Set (lsuc ℓ)` as the type of a
term that includes `Set ℓ`.
Most other functions in the standard library are also generalised to
arbitrary levels. For instance, here is the definition of composition.
```agda
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
→ (B → C) → (A → B) → A → C
(g ∘ f) x = g (f x)
```
Further information on levels can be found in the [Agda docs][docs].
[docs]: https://agda.readthedocs.io/en/v2.6.1/language/universe-levels.html
## Standard library
Definitions similar to those in this chapter can be found in the standard
library. The Agda standard library defines `_≡⟨_⟩_` as `step-≡`, [which reverses
the order of the arguments][step-≡]. The standard library also defines a syntax
macro, which is automatically imported whenever you import `step-≡`, which
recovers the original argument order:
```agda
-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
```
Here the imports are shown as comments rather than code to avoid
collisions, as mentioned in the introduction.
[step-≡]: https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v1.3.md#changes-to-how-equational-reasoning-is-implemented
## Unicode
This chapter uses the following unicode:
≡ U+2261 IDENTICAL TO (\==, \equiv)
⟨ U+27E8 MATHEMATICAL LEFT ANGLE BRACKET (\<)
⟩ U+27E9 MATHEMATICAL RIGHT ANGLE BRACKET (\>)
∎ U+220E END OF PROOF (\qed)
≐ U+2250 APPROACHES THE LIMIT (\.=)
ℓ U+2113 SCRIPT SMALL L (\ell)
⊔ U+2294 SQUARE CUP (\lub)
₀ U+2080 SUBSCRIPT ZERO (\_0)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)