This is the final part of my introduction to dependent type theory. The big theme of this article is equality though that may not be immediately obvious.

Let’s start by finally discussing function extensionality and propositional extensionality.

What’s the deal with extensionality?

Whenever we define concepts, there are basically two ways to do it: extensionally and intensionally. An extensional definition simply lists all the objects that fall under the concept to be defined. So, if I was defining what a country is, I would simply give an exhaustive list of all countries. An intensional definition, on the other hand, gives you the rules for identifying objects falling under the concept. So, an intensional definition of a country might say thing like, “it’s a distinct part of the world that has its own government.”^[1]

(As an aside, if you give a definition to a fellow human, it’s probably best to mix both kinds of definitions: “a country is a distinct part of the world that has its own government, like for example, France or Japan.”)

We can naturally extend this distinction in definition styles to the question of equality. For example, consider how the equality of two sets is defined in ZFC set theory:

\forall A \forall B ((\forall x (x \in A \Leftrightarrow x \in B)) \Rightarrow (A = B)) .

In words: two sets are equal if they have exactly the same elements. We could imagine an machine that checks all elements one by one and determines whether they’re the same in both sets, and finally tells you whether the two sets are equal.

We say that this kind of equality is extensional, because all that matters here are the contents of the sets, and we don’t care which rules were used to generate the sets. Whether the set ${2, 3, 5}$ was generated from the first three prime numbers, or the three Fibonacci numbers after $(0, 1, 1)$ , doesn’t matter for the question of equality. This makes ZFC set theory a purely extensional theory.

However, as you may remember, this is not how we defined equality in our type theory. With the way we defined equality, two functions can be non-equal even if they return exactly the same values for all inputs. I appreciate that this sounds very strange, but it’s basically due to how equality works in lambda calculus. Lambda calculus gives us these judgmental equalities (also called alpha-, beta- and eta-equivalence^[2], respectively):

\begin{matrix} (λ x . t) & \equiv (λ y . t) (λ x . t) (u) & \equiv t [u / x] f & \equiv (λ x . f (x)) \end{matrix}

where the notation in ...

FinalFantasy27

FinalFantasy27

FinalFantasy27

FinalFantasy27

FinalFantasy27

FinalFantasy27