Basic properties of identity types

Reflexivity is built into our specification of the identity type, but we really expect it to be symmetric and transitive as well. So section 2.1 of the HoTT book starts out by establishing these. The proofs were straightforward at a formal level, but intuitively, it felt like they shouldn’t work! I got that all you needed to do was essentially check it for the reflexive case, and then it would work – but that just didn’t feel like enough! It seemed like you should be able to take any path p: x = x, compose it with itself, and showed that the composition was equal to p, since that would be true if you replaced p with the identity path. I also expected this to be false, since I know that the fundamental group of the circle is \mathbb Z. Clearly, I wasn’t understanding something!

So let’s work this out carefully, and see what happens. To set things up, take a : A, and p : a =_A a. We want to try showing that p \cdot p = p is true, i.e. has an element. So encoding this as a type, we set C : \prod_{x,y : A} (x =_A y) \rightarrow \mathcal U to take x, y : A and p : x =_A y to C(x,y,p) :\equiv p\cdot p = p. Now, we need to make sure this is true in the reflexive case, i.e. we need c: \prod_{x : A} C(x,x,\mathsf{refl}_x). Expanding this out, if we are given x : A, we want to be able to construct an element of type \mathsf{refl}_x \cdot \mathsf{refl}_x = \mathsf{refl}_x. Now \mathsf{refl}_x \cdot \mathsf{refl}_x is judgementally equal to \mathsf{refl}_x, and so this type is inhabited by the reflexive object for it. So we can take c:\equiv \mathsf{refl}_{\mathsf{refl}_x}. Hence by induction, the statement is true! … right??

Did you catch the mistake? Look at C more carefully. We assumed that for any x, y : A, and p : x =_A y, that p \cdot p = p was a meaningful type. But is it? Let’s unfold the concatenation a bit. We expect p\cdot p to be a specific object of type x=_A y, which comes from a function defined by Lemma 2.1.2. So in this case, the function we need should have type (x=_A y)\rightarrow (x =_A y) \rightarrow (x =_A y). But this doesn’t represent transitivity, so it isn’t actually concatenation anymore in general – only when y is judgementally equal to x! So it is not the case that for every x, y : A and p : x =_A y, that C(x,y,p):\equiv (p\cdot p = p), because p\cdot p doesn’t always make sense! At least not for an arbitrary type A. So we can’t use path induction to prove a statement like this unless we know the type A only has one element, in which case x is judgementally equal to y.

While I was able to catch the mistake this time, it sure seems like the sort of thing that would be really easy to miss. The only reason I even caught it was because I already knew that there were fundamental groups which were non-trivial, and that these paths were supposed to have the same structure. It would be nice if there was a way to automatically catch these sorts of errors…

Advertisements

2 thoughts on “Basic properties of identity types

  1. Pingback: HoTT in Coq | Univalence Playground

  2. Pingback: Univalence Playground

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