Equality/Identity Types

Probably the most fundamental relation in logic is equality/identity. We’ve worked with it in past entries, but only now do we finally get to formally define it.

Before we get to the Agda code, we need to go back to the basics of type theory. Recall that we can interpret a type as a proposition. For example, to the proposition “the numbers \(3+4\) and \(7\) of \(\mathbb{N}\) are equal” there corresponds an equality/identity type \(3+4 \equiv_{\mathbb{N}} 7\). We can express this more generally in the form of an inference rule: “If we have two terms \(x,y\) of the same type \(A\), we can construct a new type, the equality or identity type of the form \(x \equiv_A y\).” A term of the new type is a proof of the proposition, also called an identification or certificate of identification. If there is no term, that is, if the type is empty, then its interpretation as a proposition is false.

Another way we can construct the equality/identity type is by means of a type former (essentially, a function). This is how the PLFA and the official Agda documentation define it:

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

There’s an equivalent way to define it in Agda, which is perhaps a bit easier to parse:

data _≡_ {A : Set} : A → A → Set where
  refl : {x : A} → x ≡ x

Here the type former \(\_\!\equiv\!\_\ \{A\}\) is Agda’s way of denoting \(\equiv_A\). It is a curried function into the universe \(\mathtt{Set}\), which means it represents a type family, i.e., a collection of types indexed by two terms of any type \(A\). We call this type family the equality/identity type for \(A\).¹

Its sole term constructor is \(\mathtt{refl}\). In the first definition, \(\mathtt{refl}\) appears to act as a nullary function or a constant, whereas in the second definition, it is a unary function that, given any term \(x : A\), returns a term of \(x \equiv x\), where the argument \(x\) that it was given appears on both sides of the type equality symbol. But since the argument is implicit, we can omit it, and thus the unary \(\mathtt{refl}\ \{x\}\) is the same as the nullary \(\mathtt{refl}\), both being the term/proof that any \(x\) is equal to itself.

For the sake of illustration, let’s fix the parameter type to be some type \(B\), which has only three terms: \(x,y,z\). Then the type family \(\equiv_B\) consists of the following indexed types, here arranged in a grid for easy visualization:

In this grid, \(\mathtt{refl}\) provides the term, proof or guarantee of equality/identity of every indexed type down the diagonal, i.e., \(x\equiv x\), \(y \equiv y\), and \(z \equiv z\).

If we fix the parameter to be the type \(\mathbb{N}\), then the type family would be an infinite grid, with \(\mathtt{refl}\) likewise providing the term, proof or guarantee of self-identity down the diagonal, e.g. \(1 \equiv 1, 2\equiv 2, 3\equiv 3\), etc.

The picture can be simplified if we fix one of the indices. This is what the PLFA has done in its definition by making the first index an explicit parameter enclosed between parentheses. This way the first argument will remain fixed and the second argument can vary. If we now allow the type \(\mathtt{B}\) to have an infinite number of terms, then the type family \(\_\!\equiv\!\_\ \{\mathtt{B}:\mathtt{Set}\}\ (a: \mathtt{B})\) or, in our more fancy notation, \(a\equiv_B \_\) (with the underscore indicating it accepts a single variable argument), consists of the following infinite list of indexed types:

\[ a\equiv a\quad a \equiv b\quad a\equiv c\quad \dots \]

Where \(\mathtt{refl}\) provides the term/proof of the first indexed type \(a \equiv a\).

Equivalence relation

In another entry, we demonstrated how the relation \(\_\!\leq\!\_\) is reflexive, transitive, and antisymmetric. Equality is similar: it’s reflexive (by \(\mathtt{refl}\)), transitive, but symmetric.

Symmetry

sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

To show that equality is symmetric, we must show that, for any two terms \(x\) and \(y\) of the same type \(A\), by constructing a term/proof of \(x \equiv y\) we also get a term/proof of the type \(y \equiv x\).

We do that by means of a function that we’ll call \(\mathtt{sym}\), such that, given any type \(A\) in the universe of types, and two terms \(x,y : A\), providing \(\mathtt{sym}\) with a proof of \(x\equiv y\) returns a proof of \(y \equiv x\). Let’s use currying to see how \(\mathtt{sym}\) works (we omit the implicit arguments):

\[\begin{align*} \mathtt{sym} &: x \equiv y \to y \equiv x\\ \mathtt{sym\ refl} &: x \equiv x\\ \mathtt{sym\ refl} &= \mathtt{refl} \end{align*}\]

If \(y\) really is the same as \(x\), then the type \(x \equiv y\) is actually \(x \equiv x\), whose term/proof is \(\mathtt{refl}\). In other words, by putting \(\mathtt{refl}\) as the term/proof of \(x\equiv y\), Agda makes the appropriate substitutions, such that \(x\equiv y\) becomes \(x\equiv x\), and \(y \equiv x\) becomes \(x\equiv x\). The result is that \(\mathtt{sym\ refl}\) is a term of \(x\equiv x\). But the only constructor we have for \(x\equiv x\) is \(\mathtt{refl}\). Therefore, \(\mathtt{sym\ refl}\) must be \(\mathtt{refl}\) itself.

Transitivity

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl  =  refl

The logic here is much the same as with symmetry. With currying:

\[\begin{align*} \mathtt{trans} &: x \equiv y \to y \equiv z \to x \equiv z\\ \mathtt{trans\ refl} &: x \equiv z \to x \equiv z\\ \mathtt{trans\ refl\ refl} &: x \equiv x\\ \mathtt{trans\ refl\ refl} &= \mathtt{refl} \end{align*}\]

By providing \(\mathtt{trans}\) with \(\mathtt{refl}\) as the term/proof of the type \(x\equiv y\), Agda replaces \(y\) with \(x\), so that the type \(y \equiv z\) on the second line becomes \(x \equiv z\). Then, if we provide the function \(\mathtt{trans\ refl}\) with \(\mathtt{refl}\) as proof of \(x\equiv z\), Agda replaces \(z\) with \(x\). The result is that \(\mathtt{trans\ refl\ refl}\) is a term of \(x\equiv x\). Again, the only constructor for \(x\equiv x\) is \(\mathtt{refl}\). Therefore, \(\mathtt{trans\ refl\ refl}\) must be the same as just \(\mathtt{refl}\). Pretty straightforward, isn’t it?

Reflexivity

As the PLFA notes: “Reflexivity is built-in to the definition of equality, via the constructor \(\mathtt{refl}\).” So there’s nothing to show here.

Congruence

If two objects are actually one and the same, then they remain the same after applying a function to both, because, actually, the function is applied to one thing only. Type-theoretically, if two terms \(x,y: A\) are the same, and we have a function \(f\) from type \(A\) to type \(B\), then the application of \(f\) to \(x\) and \(y\), respects that equality, i.e., \(fx = fy\) in \(B\).

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl  =  refl

With currying and implicit arguments omitted:

\[\begin{align*} \mathtt{cong} &: (f: A \to B) \to x \equiv y \to fx \equiv f y\\ \mathtt{cong}\ f &: x \equiv y \to fx \equiv f y\\ \mathtt{cong}\ f\ \mathtt{refl} &: fx \equiv fx\\ \mathtt{cong}\ f\ \mathtt{refl} &= \mathtt{refl} \end{align*}\]

The same logic applies if we have terms \(u,x: A\) and \(v,y: B\), and a function \(f\) of type \(A \to B \to C\):

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

With currying:

\[\begin{align*} \mathtt{cong}_2 &: (f: A \to B \to C) \to u \equiv x \to v \equiv y \to fuv \equiv fxy\\ \mathtt{cong}_2\ f &: u \equiv x \to v\equiv y \to fuv \equiv fxy\\ \mathtt{cong}_2\ f\ \mathtt{refl} &: v \equiv y \to f x v \equiv f x y \\ \mathtt{cong}_2\ f\ \mathtt{refl\ refl} &: f x y \equiv f x y\\ \mathtt{cong}_2\ f\ \mathtt{refl\ refl} &= \mathtt{refl} \end{align*}\]

Similarly, if two functions (or two terms of the same function type) \(f,g: A \to B\) are equal, then applying both to any term in the domain yields the same term in the codomain (again because, in reality, we are not applying two functions but only one):

cong-app : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

\[\begin{align*} \mathtt{cong\text{-}app} &: f \equiv g \to \forall (x:A) \to fx \equiv gx\\ \mathtt{cong\text{-}app}\ \mathtt{refl} &: \forall (x:A) \to fx \equiv fx\\ \mathtt{cong\text{-}app}\ \mathtt{refl}\ x &: fx \equiv fx\\ \mathtt{cong\text{-}app}\ \mathtt{refl}\ x &= \mathtt{refl} \end{align*}\]

Substitution

Equality satisfies substitution. If two objects \(x,y\) are the same, then if a predicate or property \(P\) holds of one (i.e. \(P(x)\)), then it also holds of the other (i.e., \(P(y)\)). Type-theoretically a predicate is, as we saw last time, a unary relation or, equivalently, a collection of types \(P\) indexed by the terms of another type, say \(A\). Therefore, if \(x,y: A\) are the same, then a term or proof of the indexed type \(P\ x\) is the same as a term of the indexed type \(P\ y\).

subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

With currying and \(px\) denoting a term of the type \(P\ x\):

\[\begin{align*} \mathtt{subst} &: (P : A \to \mathtt{Set}) \to x \equiv y \to P\ x \to P\ y\\ \mathtt{subst}\ P &: x \equiv y \to P\ x \to P\ y\\ \mathtt{subst}\ P\ \mathtt{refl} &: P\ x \to P\ x\\ \mathtt{subst}\ P\ \mathtt{refl}\ px &: P\ x\\ \mathtt{subst}\ P\ \mathtt{refl}\ px &= px \end{align*}\]