 Agda UALib ↑

### Equality

This is the Overture.Equality module of the Agda Universal Algebra Library.

```
{-# OPTIONS --without-K --exact-split --safe #-}

module Overture.Equality where

open import Overture.Preliminaries public

```

#### Definitional equality

Here we discuss what is probably the most important type in MLTT. It is called definitional equality. This concept is easily understood, at least heuristically, with the following slogan:

Definitional equality is the substitution-preserving equivalence relation generated by definitions.

We will make this precise below, but first let us quote from a primary source.

In An Intuitionistic Theory of Types: Predicative Part, Per Martin-Löf offers the following definition (italics added):1

Definitional equality is defined to be the equivalence relation, that is, reflexive, symmetric and transitive relation, which is generated by the principles that a definiendum is always definitionally equal to its definiens and that definitional equality is preserved under substitution.”2

To be sure we understand what this means, let `:=` denote the relation with respect to which `x` is related to `y` (denoted `x := y`) if and only if `y` is the definition of `x`. Then the definitional equality relation `≡` is the reflexive, symmetric, transitive, substitutive closure of `:=`. By subsitutive closure we mean closure under the following substitution rule.

``````    {A : 𝓤 ̇} {B : A → 𝓦 ̇} {x y : A}   x ≡ y
------------------------------------------ (subst)
B x ≡ B y
``````

The datatype we use to represent definitional equality is imported from the Identity-Type module of the Type Topology library, but apart from superficial syntactic differences, it is equivalent to the standard Paulin-Mohring style identity type found in most other Agda libraries. We repeat the definition here for easy reference.

```
module hide-refl where

data _≡_ {A : 𝓤 ̇} : A → A → 𝓤 ̇ where refl : {x : A} → x ≡ x

open import Identity-Type renaming (_≡_ to infix 0 _≡_) public

```

Whenever we need to complete a proof by simply asserting that `x` is definitionally equal to itself, we invoke `refl`. If we need to make explicit the implicit argument `x`, then we use `refl {x = x}`.

#### Identity is an equivalence relation

The `≡` type just defined is an equivalence relation and the formal proof of this fact is trivial. We don’t need to prove reflexivity since it is the defining property of `≡`. Here are the (trivial) proofs of symmetry and transitivity of `≡`.

```
≡-sym : {A : 𝓤 ̇}{x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl

≡-trans : {A : 𝓤 ̇}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl refl = refl

```

We prove that `≡` obeys the substitution rule (subst) in the next subsection (see the definition of `ap` below), but first we define some syntactic sugar that will make it easier to apply symmetry and transitivity of `≡` in proofs.3

```
module hide-sym-trans {A : 𝓤 ̇} where

_⁻¹ : {x y : A} → x ≡ y → y ≡ x
p ⁻¹ = ≡-sym p

```

If we have a proof `p : x ≡ y`, and we need a proof of `y ≡ x`, then instead of `≡-sym p` we can use the more intuitive `p ⁻¹` . Similarly, the following syntactic sugar makes abundant appeals to transitivity easier to stomach.

```
_∙_ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
p ∙ q = ≡-trans p q

```

As usual, we import the original definitions from the Type Topology library.

```
open import MGS-MLTT using (_⁻¹; _∙_) public

```

#### Transport (substitution)

Alonzo Church characterized equality by declaring two things equal iff no property (predicate) can distinguish them.4 In other terms, `x` and `y` are equal iff for all `P` we have `P x → P y`. One direction of this implication is sometimes called substitution or transport or transport along an identity. It asserts that if two objects are equal and one of them satisfies a predicate, then so does the other. A type representing this notion is defined in the `MGS-MLTT` module of the Type Topology library as follows.3

```
module hide-id-transport where

𝑖𝑑 : (A : 𝓤 ̇ ) → A → A
𝑖𝑑 A = λ x → x

transport : {A : 𝓤 ̇}(B : A → 𝓦 ̇){x y : A} → x ≡ y → B x → B y
transport B (refl {x = x}) = 𝑖𝑑 (B x)

open import MGS-MLTT using (𝑖𝑑; transport) public

```

As usual, we display definitions of existing types (here, `𝑖𝑑` and `transport`) in a hidden module and then imported their original definition from Type Topology.

A function is well defined if and only if it maps equivalent elements to a single element and we often use this nature of functions in Agda proofs. If we have a function `f : X → Y`, two elements `a b : X` of the domain, and an identity proof `p : a ≡ b`, then we obtain a proof of `f a ≡ f b` by simply applying the `ap` function like so, `ap f p : f a ≡ f b`. Escardó defines `ap` in the Type Topology library as follows.

```
module hide-ap {A : 𝓤 ̇}{B : 𝓦 ̇} where

ap : (f : A → B){x y : A} → x ≡ y → f x ≡ f y
ap f {x} p = transport (λ - → f x ≡ f -) p (refl {x = f x})

open import MGS-MLTT using (ap) public

```

Here’s a useful variation of `ap` that we borrow from the `Relation/Binary/Core.agda` module of the Agda Standard Library (transcribed into TypeTopology/UALib notation of course).

```
cong-app : {A : 𝓤 ̇}{B : A → 𝓦 ̇}{f g : Π B} → f ≡ g → ∀ x → f x ≡ g x
cong-app refl _ = refl

```

1 Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ‘73 (Bristol, 1973), 73–118, Studies in Logic and the Foundations of Mathematics, Vol. 80, 1975.

2 The definiendum is the left-hand side of a defining equation, the definiens is the right-hand side. For readers who have never generated an equivalence relation: the reflexive closure of `R ⊆ A × A `is the union of `R` and all pairs of the form `(a , a)`; the symmetric closure is the union of `R` and its inverse `{(y , x) : (x , y) ∈ R}`; we leave it to the reader to come up with the correct definition of transitive closure.

3 Unicode Hints (agda2-mode). `\^-\^1 ↝ ⁻¹`; `\Mii\Mid ↝ 𝑖𝑑`; `\. ↝ ∙`. In general, for information about a character, place the cursor over that character and type `M-x describe-char` (or `M-x h d c`).

4 Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic, (2)5:56–68, 1940 JSOR link. See also this section of Escardó’s HoTT/UF in Agda notes for a discussion of transport; cf. HoTT-Agda’s definition.