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?
