Here (section 1.12 of the HoTT book) is where things start to become more novel. We have a type for equalities between , which corresponds to the proposition that . 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 and . Or more vividly, as a path between and . 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!
- Formation rule. Given a type , and , we can form the type in the same universe. So this will give us a comparison of any two objects of a given type.
- 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 (i.e. show that is true) if we know that and are the same. So our introduction rule shall be a dependent function . You can think of this as saying that for every object of type , 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 ). Note that we get the reflexive element for if we have a judgemental equality . That’s an important part of the difference between judgemental and propositional equalities in HoTT.
- 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 as being a predicate over elements of type , i.e. a statement about an object of type , which may or may not be true depending on which specific we have. Alright, so since we are trying to define equality here, we want this to have the property if , and is true, then has to be true as well. Or in other words, we want to guarantee there is a function . 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 . These aren’t just witnesses of truth! So instead of looking at predicates over elements of type , let’s look at something that can depend on the path as well, . But now we risk showing a bit too much – we can think of this as a predicate depending on two elements of , and a path between them, and it might be the case that there are no witnesses of , maybe 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 . So once we know that is reflexive, we want to guarantee that it’s still true if we switch out with something that is equal to it. Formally, we require a function This, is path induction. This is what we can always get from an equality.
- 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 , . Remember, this is basically saying that in the case when we have the identity path , and a predicate over elements of , which we call , we have that is true whenever is true – kind of a trivial statement. This is represented by a function from to , which is what we need to specify. So the most natural choice is just to have this be the identity function for . So we say that for , the recursor can be computed for the reflexive case as We do pretty much the same thing in the inductive case. Rather conveniently, we required a function , which we can think of as saying that for all , the reflexive case of our statement is true. So given , and the reflexive path for , we want to show that is inhabited with a specific object. Naturally, we can just choose as such an object! So we say that That takes care of all the computations we need!
- 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 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!