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 , compose it with itself, and showed that the composition was equal to , since that would be true if you replaced with the identity path. I also expected this to be false, since I know that the fundamental group of the circle is . Clearly, I wasn’t understanding something!
So let’s work this out carefully, and see what happens. To set things up, take , and . We want to try showing that is true, i.e. has an element. So encoding this as a type, we set to take and to . Now, we need to make sure this is true in the reflexive case, i.e. we need . Expanding this out, if we are given , we want to be able to construct an element of type . Now is judgementally equal to , and so this type is inhabited by the reflexive object for it. So we can take . Hence by induction, the statement is true! … right??
Did you catch the mistake? Look at more carefully. We assumed that for any , and , that was a meaningful type. But is it? Let’s unfold the concatenation a bit. We expect to be a specific object of type , which comes from a function defined by Lemma 2.1.2. So in this case, the function we need should have type . But this doesn’t represent transitivity, so it isn’t actually concatenation anymore in general – only when is judgementally equal to ! So it is not the case that for every and , that , because doesn’t always make sense! At least not for an arbitrary type . So we can’t use path induction to prove a statement like this unless we know the type only has one element, in which case is judgementally equal to .
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…