3
$\begingroup$

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:

enter image description here

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?

$\endgroup$

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ Thanks for this! I'm reading your "synthetic approach to higher equalities". Just a clarifying question: When you talk about "generalizing from sets to groupoids", you are thinking of the objects of the groupoid as being analogous to elements of a single set, not as being analogous to all sets. I.e. the analogy is: A single set is analogous to a single groupoid, and the category Set is analogous to the category of all groupoids. I.e. a single Type in homotopy type theory corresponds to a single $\infty$-groupoid? $\endgroup$
    – user56834
    Jan 2, 2021 at 9:52
  • $\begingroup$ cntd. And each instance $t$ of a type $T$ is an object in the $\infty$-groupoid corresponding to $T$, where a morphism $p:t_1\to t_2$ is a proof of $t_1=t_2$, and where if we have a second order arrow $p_1\to p_2$, then that is a proof that $p_1=p_2$, i.e. these two proofs of $t_1=t_2$ are the same proof. Is this right? $\endgroup$
    – user56834
    Jan 2, 2021 at 9:55
  • $\begingroup$ Yes, that's correct. $\endgroup$ Jan 2, 2021 at 16:04
2
$\begingroup$

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 ^_^

$\endgroup$
8
  • $\begingroup$ Hi, thanks for the answer! This analogy with CW complexes is still somewhat vague to me (possibly because I have little experience with algebraic topology). Could you make more precise how actually in the case of homotopy type theory, the continuous notions relate to the underlying notions of constructible terms and proofs? (Note I've made the question statement more precise) $\endgroup$
    – user56834
    Dec 31, 2020 at 7:17
  • $\begingroup$ They don't. When working with HoTT we don't work with anything continuous, and this is part of the power of the subject. We work exclusively with the discrete descriptions of continuous objects which are given to us by a cell complex. At no point do we, for instance, work with $(0,1)$ in HoTT. One can of course, but the subject takes topological spaces to be the "default objects". $\endgroup$ Dec 31, 2020 at 7:19
  • $\begingroup$ In Set Theory we have sets, and we have to endow those sets with a topology to give them geometric meaning. In HoTT, types come with a topology by default, and sets correspond to types with the discrete topology. The reason there's no visible continuous mathematics is because we have a nice finitary description of the continuous objects. Moreover, it turns out that by working with the description instead of the object itself, we can use different tools to study the object that would ordinarily be unavailable due to the continuous nature of the object. $\endgroup$ Dec 31, 2020 at 7:22
  • $\begingroup$ Then I'm confused about what the point is of even talking about those continuous objects in the context of HoTT. My understanding is that the primary motivation HoTT for Voevodsky (or at least for me it is) was to provide a foundational framework within which to do mathematics, and that can in principle be done using a proof assistant like Coq. Essentially I think of HoTT as an extension of the Calculus of Constructions with some more powerful tools (in particular my understanding is the main additions are this proof-relevant interpretation of identity types, and the univalence axiom) $\endgroup$
    – user56834
    Dec 31, 2020 at 7:30
  • $\begingroup$ cntd. So my understanding is that the point of introducing the notion of homotopy, is to be able to talk about whether two proofs are equal. But if we can talk about whether two proofs are equal without actually talking about these continuous spaces with homotopies, and just talking about the actual proof terms, why do people in HoTT talk about them? Is it just a useful intuitive mental model? My guess is it's more than that. $\endgroup$
    – user56834
    Dec 31, 2020 at 7:33

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.