1
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ What about something like, for any $p,q : x = y$, $p = q$? $\endgroup$
    – ToucanIan
    May 25 at 15:27
  • $\begingroup$ @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. $\endgroup$ May 25 at 15:53
  • $\begingroup$ Thanks! That makes sense. $\endgroup$
    – ToucanIan
    May 25 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.