Identity types

Here (section 1.12 of the HoTT book) is where things start to become more novel. We have a type x =_A y for equalities between x, y :A, which corresponds to the proposition that x = y. An object of this type means the equality is true – but there is more information here! We can think of the different objects of this type as being different ways we can identify our x and y. Or more vividly, as a path between x and y. Each path is a witness of the veracity of the equality, that is, a proof. This is a really compelling idea, but I think it will take some time for it to sink in at an intuitive level.

Remember that we have a general pattern for specifying a type. Since identity types are a more subtle concept than the other types we have seen so far, let’s write this all out carefully. If you still feel confused about the distinction between elimination and computation (as I was when I wrote the first draft of this post), you should read my post where I explore this issue.  Anyway, here we go!

  1. Formation rule. Given a type A : \mathcal U, and a, b : A, we can form the type (a =_A b) :\mathcal U in the same universe. So this will give us a comparison of any two objects of a given type.
  2. Introduction rule. To make this type worthy of being called the identity type, we need an introduction rule that captures this idea properly. Intuitively, it seems like we should be able to make an element of (a =_A b) (i.e. show that a = b is true) if we know that a and b are the same. So our introduction rule shall be a dependent function \mathsf {refl} : \prod_{a : A} (a =_A a). You can think of this as saying that for every object a of type A, a = a is true. Or in other words, this comparison that we are defining has the property that it is reflexive (which is why we call this function \mathsf {refl}). Note that we get the reflexive element for (a =_A b) if we have a judgemental equality a:\equiv b. That’s an important part of the difference between judgemental and propositional equalities in HoTT.
  3. Elimination rules. But just because our comparison is reflexive doesn’t mean it is a good notion of equality. We also need to know what we can do with an equality. Well, intuitively, if we know two things are equal, we can substitute one with the other, and expect all the same things to be true. So how do we encode this as a rule? Let’s think of C : A \rightarrow \mathcal U as being a predicate over elements of type A, i.e. a statement about an object a of type A, which may or may not be true depending on which specific a we have. Alright, so since we are trying to define equality here, we want this to have the property if x =_A y, and C(x) is true, then C(y) has to be true as well. Or in other words, we want to guarantee there is a function \displaystyle\mathsf{rec}_{=_A} : \prod_{x y: A}\prod_{p:x=_A y}C(x)\rightarrow C(y). Viola! This is the recursor for the identity type. That’s pretty cool. But we can dream larger!! These aren’t mere propositions! We have all this potential extra structure lying at our feet, the different paths between two of our elements of A. These aren’t just witnesses of truth! So instead of looking at predicates over elements of type A, let’s look at something that can depend on the path as well, C : \prod_{x, y:A}(x=_A y) \rightarrow \mathcal U. But now we risk showing a bit too much – we can think of this as a predicate depending on two elements x, y of A, and a path p : x =_A y between them, and it might be the case that there are no witnesses of C(x,x,\mathsf{refl}_x), maybe C is just constantly the empty type. But equality is reflexive! So we want to make sure that whatever we are talking about, it is something which is true in the reflexive case. Hence, we’ll also require a function c:\prod_{x :A}C(x,x,\mathsf{refl}_x). So once we know that C is reflexive, we want to guarantee that it’s still true if we switch out x with something that is equal to it. Formally, we require a function \displaystyle\mathsf{ind}_{=_A}: \prod_{C: \prod_{x, y:A}(x=_A y) \rightarrow\mathcal U}\prod_{x:A}C(x,x,\mathsf{refl}_x)\rightarrow\prod_{x, y:A}\prod_{p: x=_A y}C(x,y,p). This, is path induction. This is what we can always get from an equality.
  4. Computation rules. Well we have these awesome recursor and inductor objects, but we aren’t really done until we’ve defined how they act on objects defined by our introduction rule. Fortunately, this is a lot easier to do than determining the elimination rules. For the recursor, this means we need to specify for x:A, \mathsf{rec}_{=_A}(x,x,\mathsf{refl}_x). Remember, this is basically saying that in the case when we have the identity path \mathsf{refl}_x, and a predicate over elements of A, which we call C, we have that C(x) is true whenever C(x) is true – kind of a trivial statement. This is represented by a function from C(x) to C(x), which is what we need to specify. So the most natural choice is just to have this be the identity function for C(x). So we say that for x:A, the recursor can be computed for the reflexive case as \mathsf{rec}_{=_A}(x,x,\mathsf{refl}_x):\equiv \mathsf{id}_{C(x)}. We do pretty much the same thing in the inductive case. Rather conveniently, we required a function c:\prod_{x : A}C(x,x,\mathsf{refl}_x), which we can think of as saying that for all x : A, the reflexive case of our statement C is true. So given x : A, and the reflexive path for x, we want to show that C(x,x,\mathsf{refl}_x) is inhabited with a specific object. Naturally, we can just choose c(x) as such an object! So we say that \displaystyle\mathsf{ind}_{=_A}(C,c,x,x,\mathsf{refl}_x):\equiv c(x). That takes care of all the computations we need!
  5. Uniqueness principle. I don’t quite understand the uniqueness principle yet, but luckily, the identity type doesn’t need one to specify it! If I’m understanding things correctly, its absence is significant, since it ultimately allows there to be a richer homotopy structure – I think the univalence axiom might even play into this. But I don’t really know much about that stuff yet, so take this speculation with a grain of salt.

So that fully specifies the identity type. Great! I’ll briefly mention that there is also an equivalent induction for it called based path induction, where you stick with a certain base element the whole time for one end of all your paths, which can make things more convenient sometimes. Oh yeah, and you can make a disequality type by taking the negation of an identity type.

One thing to keep in mind about identity types is that we only specify the computation rule in the reflexive case. So if we want to prove a statement which depends on something with an identity type, we only have to show that it is true in the reflexive case, since that is enough to show the right inductor exists (with the little c function), and it’s the only case where it is forced to be a certain thing. We’ll see a lot more of this in chapter 2, so don’t worry!


Leave a Reply

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

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

Google+ photo

You are commenting using your Google+ 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 )


Connecting to %s