In Homotopy Type Theory, how do the continuous notions of spaces and paths, match the discrete notions of constructible terms and proofs?

Question

Context: I'm starting with being interested in type theory as a framework within which to do mathematics (e.g. practically, using proof assistants based on type theory), and my understanding is that HoTT is motivated partially/primarily from that perspective. I and am not interested in homotopy theory per se, or in using type theory to understand homotopy theory.

My understanding of homotopy type theory is limited, but I know that in HoTT we think of a type $T$ as a space, of instances $x,y:T$ of the type as points in that space, and of proofs $p:x=_Ty$ of equality as paths in the space.

How I can understand "proofs of equality as paths"

My interpretation of proofs of equality is that they are computational paths between terms. If we think of $x$ and $y$ as actual constructed terms in e.g. a proof assistant such as Coq, then the way to prove $x=_Ty$ is to show a sequence of computational steps (or at least, a program that would produce one, such as in an inductive proof) from $x$ to $y$. E.g. with the standard inductive definition of the natural numbers, it could be a transformation from $(1+1)+1$ (i.e. $x$) to $3$ (i.e. $y$), by repeatedly applying the addition rules to get $s (s (s (0)))$ and then applying the definition of $3$. i.e. proofs of $x=_Ty$ are computationally valid paths between terms, using the underlying computational system's (lambda calculus I'd presume) valid computation rules (e.g. beta-reduction, delta-reduction of lambda-terms).

So the way I think of it is: two terms may be different syntactically (e.g. $1+1$ and $2$), and are therefore different points in the "space belonging to their type" (e.g. $\mathbb N$). But they are semantically equal to each other, so that there is a computational path between them.

proofs of equality in homotopy type theory

In explanations of homotopy type theory that I've seen, the explanation usually asks you to think of types as spaces, where usually they are pictured as topological spaces (circles, donuts, etc). Then the point is made that two proofs $p,q:x=_Ty$ are fundamentally different, if there is no homotopy between them, and some image like this is shown to suggest that two proofs are not homotopic:

But afaik, a homotopy has to be continuous, meaning that the space has to have some kind of topological structure. However, the computational steps that we make in reasoning e.g. that $(1+1)+1 = 3$, are finite. My understanding is that it's fundamental to intuitionistic type theory that all the terms of a type are actually constructible terms, i.e. strings of symbols that we can write down, and hence that the "space" belonging to a type $T$ is discrete. But the only reasonable topology that I can think of on such a space would be the topology generated by the base set consisting of equivalence classes of terms based on $=_T$, which would I think imply that all paths $p,q:x=_Ty$ are homotopy equivalent (since any path consisting of points inside such a base set is continuous).

This makes me confused about homotopy type theory itself: It seems to me that in order to formalize the idea of proofs being fundamentally different, we'd have to think of a discrete object, probably a finite graph (where nodes are terms and links are basic computational steps), and concepts like homotopy and continuous functions and spaces are out of place.

Where is the mistake in my thinking?

Answer 1

I would say there is no mistake in your thinking. Rather, the mistake happened many decades ago when algebraic topologists gradually came to use the word "space" for a discrete object that should really be called an "$\infty$-groupoid". The correct thing to say is then that HoTT interprets types as $\infty$-groupoids (though not, of course, necessarily finite ones). This is even true semantically: all the formal mathematical interpretations of HoTT sending types to "spaces" actually use structures such as simplicial sets or cubical sets, which are discrete objects --- it's just that homotopy theorists have come to abuse the word "space" to refer to those things rather than to actual topological spaces.

The reason the word "space" took on this meaning is that topological spaces can be used as presentations of $\infty$-groupoids via a construction called the "fundamental $\infty$-groupoid of a space", and (at least, assuming classical logic) every $\infty$-groupoid is equivalent to one arising in this way. Moreover, the fundamental $\infty$-groupoid of a space remembers (and is "determined by", in an appropriate sense) all of the algebraic invariants constructible from a topological space, and so algebraic topologists studying these invariants came gradually to identify a topological space with its fundamental $\infty$-groupoid --- and this was historically before anyone had given a precise definition of $\infty$-groupoid at all.

However, nowadays this conflation of spaces with $\infty$-groupoids has real dangers, one of which is the difficulty of intuition that you've run across. Another is that we also sometimes want to study spatial $\infty$-groupoids, i.e. $\infty$-groupoids that also have an additional topology on their underlying sets that's unrelated to their $\infty$-groupoid structure, and if "space" means $\infty$-groupoid then that gets very confusing.

I have written some introductions to HoTT that emphasize this perspective, called A synthetic approach to higher equalities and The logic of space.

Answer 2

It's quite common to describe "nice" topological spaces (up to homotopy) by cell complexes. The idea is to specify your space by combinatorial data, and we can then use combinatorial reasoning to prove things about our spaces.

We have $0$-cells, or points. Then we have $1$-cells, which are edges connecting the points. If we have a bunch of edges which enclose a region (a polygon, say) then we can "fill" the region with a $2$-cell.

As an example, we can build the circle $S^1$ by considering one $0$-cell $\mathtt{base}$, and one $1$-cell $\mathtt{loop}$ connecting $\mathtt{base}$ to itself. If we then add a $2$-cell to this, we would get a disk $D^2$. If we add two $2$-cells, we get a sphere $S^2$. Here the original $S^1$ is the equator, and the two $2$-cells become the hemispheres. As a (fun?) exercise, you might try to build a cellular complex which describes a Torus.

Notice this is an entirely combinatorial description. We have $n$-cells in various dimensions, and we have incidence relations telling us how these cells are glued together. We're not reasoning about open sets, or actually thinking of our edges as copies of $(0,1)$. We really do have a discrete description of these topological objects, and this description is frequently more user-friendly than the classical one when it comes to explicit computations. Of course, we can cash out this description and talk about a honest topological space by putting the weak topology on the collection of cells.

Topologists already cared about cell complexes, because they let us efficiently read off topological invariants. By studying fudamental groups in this way, for instance, we are led naturally to combinatorial group theory. We can also read off more complex invariants using cellular homology. All this to say that these cellular decompositions have been of interest to topologists for a long time.

---

What, then, is type theory?

Given a type $A$, we can construct terms $a : A$ that inhabit $A$. Of course, some terms are syntactically different, but describe "the same thing", and we might want to consider them equal. So we postulate an Identity Type whose terms are "proofs" that $a_1 = a_2$.

Now let's say we have a type $A$. Let's say it has one constructor $\mathtt{base} : A$. But let's give it a higher order constructor as well. We'll give it a nontrivial proof $\mathtt{loop} : \mathtt{base} = \mathtt{base}$. If you think the data of this type sounds a lot like the data of a cellular decomposition of $S^1$, you're exactly right!

This, then, is the way that HoTT works. Using Higher Inductive Types we can consider types which have exactly the same data as the cellular decomposition of topological spaces. Then by using type theoretic arguments (for instance, path induction), we can prove things about topological spaces!

---

Rather excitingly, the correspondence goes both ways. Type Theories correspond to the internal logics of categories, and it turns out these logics can be understood geometrically by reasoning with cell complexes. When we draw a commutative diagram, we have objects ($0$-cells) which we connect by arrows ($1$-cells). Then saying the diagram commutes is akin to saying we can "fill it in" by a $2$-cell. But what if we have multiple ways for the diagram to commute? For instance, if we have a "pullback cube" (where we pull back an entire pullback square along an arrow $f$). Then there are two natural transformations which witness a certain commutativity, and these natural transformations are actually isomorphic too. We say that this is a $3$-cell which "fills the cube". Obviously you can continue on in this way, and if you've heard people talk about "Infinity Categories" this is roughly what they're studying.

This is why you see so many higher category theorists also excited about algebraic topology -- the two fields are deeply connected in precisely this way. The study of these higher categories is entirely analogous to the study of cell complexes, and there's a lot of very pretty interplay between the fields.

---

I hope this helps ^_^