Identity types and how to use them

I had a snappy line at the end of my discussion of sums and products, so I figured it was as good a place as any to stop. After this post, I’ll need one more post to clean up a few things, and then my mini tutorial on type theory will be over. Today, we’re talking about equality, which is probably the hardest part of Martin-Löf type theory.

Equality in logic

When you first learn first-order logic, you learn how to generate a first order language which has:

  • Variables
  • “Logical symbols”, (,),\rightarrow,\wedge,\vee, \forall, \exists, and crucially equality, =.
  • Relation symbols and function symbols. (Also constant, symbols, but these are “nullary” functions).

For a long time it struck me as somewhat strange that equality was included here; after all, isn’t equality just another relation? What makes equality so special? But as I’ve become more familiar with logic and models, and the subtle interplay between object language and metalanguage, I’ve slowly come to understand why equality is often treated as a logical symbol. The very short version is that working with equality almost always happens at the level of our logic (that is, the meta in first order logic). In particular, we want a few things to be true:

  • We can substitute equal objects for equal; If \varphi(x) holds, and x=y, then \varphi(y) holds. This (Leibniz Law) seems silly and obvious, but it is something we need to prove, and it’s something we need to prove at the level of the logic (since it deals with formulas) if we use equality as a relation symbol, we need to prove this separately for every theory.
  • We want equality to be “the least congruence” on a model. But not all congruences are even definable in a given theory, so it’s not clear that such a statement can be reasonably made anywhere besides the logical level.

The point of all this is to say that if we’re trying to give an account of (mathematical) logic, we really do need to include equalities. It was also to point out two important properties of equality:

  • Minimality
  • Leibniz Law

We will use the first of these properties (minimality) as the basis of our definition, but some features of type theory will allow us to state something more general and without making any appeal at all to congruences.

Minimality

One of the curious properties of type theory is that the logic happens at the object level. We encode logical prepositions as types, as objects in or system; and proofs as terms, again objects in our system. So, since we will give our account of equality at the logical level, it is also going to be an object: a type. That is, for any two terms \mathsf{x} and \mathsf{y}, we will have a type \mathsf{x=y}.

But hold on: unlike in set theory, we can’t pick objects out of nowhere: to have an object means to have an object of some type. But it hardly makes sense to compare objects of different types, so we have the formation rule for equality (or identity, as type theorists usually call it):

Identity formation: If x:A and y:A, then x=y is a type. Note that I haven’t said this type is inhabited, only that it exists—thinking in terms of propositions, we’re saying that it makes sense to propose x=y (although it may be false). Sometimes it’s helpful to denote the type at which this equality lives. In that case, I’ll write a subscript, \mathsf{x}=_{\mathsf{A}}\mathsf{y}.

Now we need an introduction rule. There’s an obvious candidate: anything must be equal to itself. That is, equality is reflexive. This seems like the bare minimum we could ask of equality, so we have

Identity introduction: for any x:A, there is a term \mathsf{refl}:x=x. When we need to be clear, I’ll put a subscript, \mathsf{refl}_{x}.

Next is the elimination rule, which is a little more subtle. Here we have to return to that notion of minimality: we will say that identity is the “least reflexive relation”. If you are a type theorists, you can already guess what the elimination rule will be from that statement. But if you’re reading this, I’m going to guess you’re not a type theorist. As is common in math, we have to express “minimality” in an indirect way. As a first approximation, consider a binary relation on some type A. We can view this as a function R:A \rightarrow A \rightarrow \mathsf{Type} since it takes two elements of A and returns a proposition. Since we can talk about equality, there are two ways to say that a relation is reflexive, which I’ll call “strong” and “weak” (this is my own terminology, so you won’t find anything by looking it up; you’ll probably find something about lattices):

  • weak reflexivity: For any x:A, R(x,x). That is, every term is related to itself. In typical type theory notation, we’d write this as \prod_{x:A}R(x,x).
  • strong reflexivity: For any x,y:A, we have x=y \rightarrow R(x,y). That is, equal terms are related. Again in standard notation, \prod_{x,y:A}(x=_{A}y \rightarrow R(x,y)).

The second is “strong” because it implies the other: if r is a proof that R is strongly reflexive, then \lambda x.r(x,x,\mathsf{refl}) (the function taking x to the proof that R(x,x), since we know \mathsf{refl}:x=x) is a proof that R is weakly reflexive. Our first attempt at an elimination rule:

Identity elimination (almost): if R is a weakly reflexive relation on A, then R is strongly reflexive. Or, more in the spirit of the other elimination rules I’ve given:

Let R:A \rightarrow A \rightarrow\mathsf{Type}, and r:\prod_{x:A}R(x,x). Then there is r' :\prod_{x,y:A}R(x,y).

We’ll skip the computation rule for now; I’ll come back to it when I give the full form of the elimination rule. In the meantime, this is actually enough to do a surprising amount

Symmetry, transitivity, and a little more

We can actually use this form of the elimination rule to show symmetry and transitivity.

Equality is symmetric.

Proof: The statement of symmetry is \prod_{x,y:A}x=y\rightarrow y=x. Observe that this precisely says that the “flipped identity type” R(x,y) :\equiv y=x is “strongly reflexive”. So, to apply the elimination rule we only need to show that it is weakly reflexive. That is, \prod_{x:A}x=x. But this is exactly what \mathsf{refl} gives us.

Equality is transitive.

Proof: This is similar: we want to show \prod_{x,y,z:A}x=y\rightarrow y=z\rightarrow x=z. Reordering the arguments, we want to show \prod_{x,y:A}x=y\rightarrow\prod_{z:A}y=z\rightarrow x=z. So, if we let R(x,y) :\equiv \prod_{z:A}y=z\rightarrow x=z, we want want to show that R is strongly reflexive. But by identity elimination, we only need to show it’s weakly reflexive. That is, we need a function \prod_{x:A}\prod_{z:A}x=z\rightarrow x=z. From here we could eliminate again, but we might as well take the pointwise identity function f(x,p) :\equiv p. (f :\equiv \lambda x.\lambda p . p). And so we have that R is weakly reflexive, and by identity elimination, we are done. (aside: we need to be careful when reordering arguments like we did here. We need to make sure that the later arguments don’t depend on earlier ones. Since x=y doesn’t depend on z, this is safe.)

In fact, we can do more than this. Remember earlier I mentioned that a crucial property of equality is the Leibniz law: If P(x) and x=y, then P(y). We can actually prove this!

Let x,y:A and P:A\rightarrow \mathsf{Type}. Then there is a function x=y\rightarrow P(x)\rightarrow P(y).

Proof. Take R(x,y) :\equiv P(x)\rightarrow P(y). This is weakly reflexive, since \lambda p.p : P(x)\rightarrow P(x), and so by identity elimination is strongly reflexive. I.e., for all x,y:A, x=y\rightarrow P(x)\rightarrow P(y).

A nice exercise is to rewrite the proofs of symmetry and transitivity using the Leibniz law (instead of using identity elimination directly).

We can do better still: we can actually show that for any function f:A\rightarrow B, if x=_{A}y, then f(x)=_{B}f(y). Specialized to B=\mathsf{Type}, this says that not only do we have a function from P(x) to P(y), but that P(x)=P(y). The proof is again by identity elimination: we only need to show that for any x, f(x)=f(x), but we have \mathsf{refl}_{f(x)}.

Let’s back up a bit: when we write out all of these theorems formally in type-theoretic notation, we see that in each case we have a function:

  • We have inversion x=y\rightarrow y=x, and we write the inverse of p:x=y as p^{-1}:y=x,
  • We have concatenation x=y\rightarrow y=x \rightarrow x=z, and we write the concatenation of p:x=y and q:y=z as p\cdot q:x=z
  • We have a function which “transports elements of P(x) along an equality” (p:x=y) to elements of P(y). We write this function \mathsf{transport}^P(p,u) (here p:x=y and u:P(x).)
  • We can “apply functions to equalities” which we write \mathsf{ap}_f(p) (or sometimes just f(p)), so \mathsf{ap}_f:x=y\rightarrow f(x)=f(y).

If I had given you the computation rule, you could show that these have the properties we expect inverses, concatenation, and so on to have. (technical stuff: were we to prove these properties, we’d have proven that types form groupoids, with equalities as morphisms, and functions as functors. We almost have that type families are fibrations, but we’re not quite there yet.)

Dependent elimination

I said the elimination principle I gave wasn’t quite the full principle. So, what can’t we do?

Well, suppose we want to generalize \mathsf{ap} to work on dependent functions. When we try to write out this statement, we run into a problem. Let f:\prod_{x:A}B(x). We want to say f(x) = f(y). But f(x):B(x) and f(y):B(y). A priori these are different types. But, we can solve this by transporting: since we have p:x=y, we can transport f(x) along p to get some element of B(y). This element is what should be equal to f(y). So the full statement becomes

Given a type A, a family B:A\rightarrow\mathsf{Type}, and a dependent function f:\prod_{x:A}B(x), for any x,y:A, there is a function \mathsf{apd}_f:\prod_{p:x=y}\mathsf{transport}^B(p,f(x)) = f(y).

Trying to prove this we run into a problem: our function \mathsf{apd}_f is a dependent function. But we’ve only given an elimination rule for non-dependent functions. So, we need a dependent eliminator, just like we did for \Sigma types last time. Morally, we eliminate exactly as we did before, but the type encoding “reflexivity” also depends now on the equality we give it. So, we have:

Identity elimination: Let C:\prod_{x,y:A}(x=y\rightarrow \mathsf{Type}) and suppose we have c:\prod_{x:A}C(x,x,\mathsf{refl}) (“C is weakly reflexive”). Then we have r:\prod_{x,y:A}\prod_{p:x=y}C(x,y,p) such that

Identity computation: r(x,x,\mathsf{refl}) \equiv c(x).

Now, we can construct \mathsf{apd}_f (almost) exactly how we constructed \mathsf{ap}. We need only construct \prod_{x:A}\mathsf{transport}^B(\mathsf{refl},f(x)) = f(x). But a quick check of the definitions (using our new computation rule) shows us that \mathsf{transport}^B(\mathsf{refl},f(x)) \equiv f(x) definitionally. So we can use \mathsf{refl}.

From here there’s a lot we can do. In fact, with the dependent sums and products we introduced last time, we now have all of the “usual” types of dependent type theory. But I think we’ve seen quite enough for one post.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s