In homotopy type theory, what are the intermediate values along a path?

Question

I'm having a hard time understanding how the continuous notion of a path applies to homotopy type theory.

I understand that from topology, a path is a continuous function $f : [0,1] \to X$ from the unit interval in $\mathbb{R}$ to a space $X$. A homotopy can be defined as a path between two continuous functions.

In homotopy type theory, a path $p : a = b$ is a proof of equivalence between two points, $a$ and $b$. It's clear to me that the left endpoint of the path, at 0, would be $a$, and the right endpoint, at 1, would be $b$. But since this is a real interval, there must be some point at, say, $\frac{1}{2}$, or $\frac{1}{\pi}$.

For example, suppose that we have a type of arithmetic expressions. One point would be $2 + 1$ and another would be $3$. These should be equivalent, so there must be a path between them. I know what a proof of such a proposition would look like, in Peano arithmetic. But I have no idea how to conceptualize that as a function from the unit interval.

Perhaps the answer is: These paths in homotopy type theory are proofs, and there is no analogy to functions from the unit interval. But if there is no such analogy, then what's the use of invoking the idea of paths at all?

Answer 1

The problem is that you are not asking a homotopy-invariant question about paths. In homotopy theory we think about paths up to homotopy equivalence relative to the endpoints, so it's a homotopy-invariant question to ask what the start and end of a path are (or at least, more precisely, what path component they're in), but it's not a homotopy-invariant question to ask what, say, $p \left( \frac{1}{2} \right)$ is, because a homotopy can change that value arbitrarily (it can be any point in the same path component as the endpoints). Homotopy type theory by construction discusses homotopy-invariant questions only so this is not the sort of question you can or should ask in it.

This is somewhat analogous to how in functional analysis elements of $L^p$-spaces are not functions and it's not a meaningful question to ask what their value is at a point, because one can arbitrarily modify the values of $f \in L^p$ on a set of measure zero.

All of this will get clearer if you spend some time studying ordinary homotopy theory, particularly the relationship between a group $G$ and its classifying space $BG$ as a special case of understanding the homotopy hypothesis. This previous question and the answer by Mike Shulman may also be helpful, in clarifying the difference between a topological space and a homotopy type.

Answer 2

Qiaochu Yuan’s answer is excellent so I won’t repeat its points, but to add a little more, responding especially your last sentence: There is a strong analogy between paths in HoTT and paths in classical homotopy theory, but that analogy does not include the notion of “intermediate values” in the way you’re asking for.

Indeed, it’s not just in HoTT that “intermediate values” are discarded — much of modern homotopy theory is based on simplicial sets as well as, or instead of, topological spaces. Simplicial sets, too, have no “intermediate values” in paths: roughly, they’re certain algebraic/combinatorial objects, a higher-dimensional generalisation of directed multigraphs, and their paths are like the edges in such a graph — just combinatorial specifications “an edge/path from $x$ to $y$”, so again, with no intermediate values. There is a simplicial set with just two vertices $x$, $y$, and a path from $x$ to $y$.

Answer 3

I'm not sure if I'm just thinking about it from too much of a physicist's and functional programmer's standpoint, but to me the “intermediate steps” are transformation steps within the proof. For example, $p: (5 + 3 = 3 + 5)$ might have $$\begin{align} p(0) = 5+3 \\ p(\tfrac12) = 4+4 \\ p(1) = 3+5 \end{align}$$ ...which could be further divided in $$\begin{align} p(\tfrac14) = (4+1)+(3+1) \\ p(\tfrac34) = (3+1)+(4+1) \end{align}$$ and so on. Of course, in the end you're not really interested in all the intermediate steps, which is the whole point of forming a single theorem: it must hold under any proof of this type, i.e. it's invariant under what particular path between the end points you choose.

Like in general topology, you can string two paths together and get a new path (which in the middle uses the result of the first theorem), as well as split up any path in two paths – though unlike in topology, it is not defined what the mid point in a given path is, and therefore you can't really write expressions like $p(\tfrac12)$, in general. In particular, an axiom can only be decomposed into a concatenation of the axiom itself with the identity proof.