# HoTT informal path induction

As before I'm still exploring HoTT. While turning more to the informal everyday view on it, I have found an issue I cannot solve by my own.

Proving by path induction can be done formal by invoking the induction principle or even more technical: using the $$\mathsf{ind}_=$$ method. But it can be also done using the informal way. Consider, for example the associativity of path concatenation:

### Associativity of Path Concatenation

For any $$p : x = y$$, $$q : y = z$$ and $$r : z = w$$ it holds that $$p \centerdot (q \centerdot r) = (p \centerdot q) \centerdot r$$

where $$\centerdot$$ is the path concatenation.

In the HoTT Book there is an informal proof which is stated as follows:

### Proof

By induction, it suffices to assume $$p,q$$ and $$r$$ are all $$\mathsf{refl}_x$$. But in this case, we have: \begin{align*} p\centerdot (q\centerdot r) &\equiv\mathsf{refl}_x\centerdot(\mathsf{refl}_x\centerdot \mathsf{refl}_x)\\ &\equiv \mathsf{refl}_x\\ &\equiv (\mathsf{refl}_x\centerdot\mathsf{refl}_x)\centerdot\mathsf{refl}_x\\ &\equiv (p\centerdot q)\centerdot r \end{align*}

### What wonders me

So why not conclude $$(q \centerdot r) \centerdot p$$ here, for example, since every one of these are judgementally equal to $$\mathsf{refl}_x$$ in this particular case?

### Own ideas

My guess is, that each $$\mathsf{refl}_x$$ is associated with $$p,q,r$$ resp. in some "syntactic sugar way" since after all this informal method is basically just an abbreviation for the formal way. But it looks quite fishy.

### Questions

Would this be an explanation? And therefore: when proving informally with several path inductions it's best to keep track of which $$\mathsf{refl}_x$$ belongs to which path?

## 1 Answer

The reason you can't prove $$p\cdot (q\cdot r) = (q\cdot r)\cdot p$$ by path induction is that for general $$p,q,r$$, the statement is ill-typed. It doesn't matter that it becomes well-typed and true after replacing all the paths by refl. Path induction only applies to a statement that's well-typed in the general case, and becomes true when replacing the path(s) by refl.

• What about something like, for any $p,q : x = y$, $p = q$? May 25 at 15:27
• @ToucanIan You have to do path induction one path at a time. After path induction on $q$ (say), your statement becomes "for any $p:x=x$, $p=\mathsf{refl}_x$". Now you can't do a further induction over $p$ because $p$ no longer has a general path-type but its two endpoints are constrained to be the same. May 25 at 15:53
• Thanks! That makes sense. May 25 at 15:55