The Homotopy Type of Mathematics

Let $X$ be a topological space. If $X$ is nice enough, then we can think of the data of the “homotopy type” of $X$ as follows:

We have the points of $X$;

For every pair of points $x, y \in X$, we have the paths from $x$ to $y$;

For every pair of paths $\gamma_0, \gamma_1: x \rightsquigarrow y$ we have the different ways of interpolating between $\gamma_1$ and $\gamma_2$, namely, paths $\gamma_\tau: x \rightsquigarrow y$, depending continuously on the parameter $\tau \in [0,1]$, so that $(\gamma_\tau)_{\tau = i} = \gamma_i$ for $i=0,1$; we can think of these as paths in the space of paths from $\gamma_0$ to $\gamma_1$;

For every pair of interpolations from $\gamma_0$ to $\gamma_1$ one has the various interpolations between the interpolations, …

“and so on”.

The above paragraph is supposed to intuitively describe a mathematical concept; of course, it’s not quite mathematics because of the “and so on” at the end. (It is so easy to get away with lazy thinking!) The basic idea presumably goes back to the origins of the idea of topology; the importance of formalizing this idea was emphasized by Grothendieck in “Pursuing Stacks”, or at least, so people seem to say; over the past three decades or so, many people have worked on turning the above intuitive description into rigorous mathematics.

The reason this idea is tricky, and powerful, is as follows. In a “space” $X$, if I have a path $\gamma: x \rightsquigarrow y$, then I probably have a corresponding “backwards path”. But the previous section never required the paths to be invertible! A common situation where non-invertible “paths” show up is when we think of
$X$, instead, as the “collection of topological spaces””; the “paths” are now functions between topological spaces; the “interpolations between paths” are the continuous deformations from one function to another, also called the “homotopies”; “and so on”. Generally, one could say that the kind of structure described in the previous section naturally arises when one has some things, and some relationships between those things, but maybe to describe a relationship one has to make some choices, so then one must keep track of the way the different choices could have been made, and the relationships between those choices… “and so on”.

In mathematics, as in life, one cannot avoid making choices, and one cannot avoid paying for them later.

This idea goes by the name of “$\infty$-category theory”, and it is far from a finalized area of mathematics. It sounds simple enough, but the second one makes a choice of formalism, one gets trapped in brutal combinatorical complexity when one tries to prove statements that “sound obvious”. The currently most popular formalization of the idea of allowing just the the paths to be non-invertible, while forcing all “higher interpolations” to be invertible, is the theory of quasicategories, which traces its lineage to Boardman-Vogt, and was significantly developed by Joyal and then by Lurie in several opuses of several thousand pages. This theory has had a major impact on mathematics and is central to contemporary advances in arithmetic geometry, representation theory, and symplectic geometry. There are clear applications of the theory where one allows the first interpolations between paths to be non-invertible; but already here it is quite difficult to find mathematicians that are familiar with the technicalities and the status of the theory, in as much as it exists. Emily Riehl’s work is supposed to have put the basic theory on solid foundations, although I’ve never had a long coversation with someone who understands her work. Before her work, certain foundations were created in a book of Gaitsgory and Rozenblym, and a large chunk of the subject of Geometric Representation Theory relies on these foundations; but they are somewhat controversial, because many crucial technical statements in this book are given little proof, and while these technical statements are widely believed, category theorists have tried to prove them and so far many have failed – the combinatorical complexity is simply too high. (This “controversy” I have only heard through gossip, and the only written record I have seen is certain remarks in the homotopy-theory chatroom on MathOverflow. The sociology of MathOverflow may be the subject of a later post.)

People have combinatorical models which allow the higher interpolations to be non-invertible, but as far as I know the theory is in its very infancy. We are still pursuing (yet ever Higher) Stacks.

Certain aspects of this theory are also popular in the computer science community. This is amazing because of the resulting clash of cultures. This clash is beautifully illustrated in the amazingly long comment section to this post.

Category Theory was born from the Cronus of Cohomology Theory, and Higher Category Theory from Homotopy Theory and Algebraic Geometry; but Algebraic Geometry has always been tight with Model Theory (just think of the Lefshetz Principle! and Lefshetz “never gave a correct proof nor stated an incorrect theorem”), and Grothendieck’s Topos Theory geometrized Mathematical Logic… Computer Science, too, came from Mathematical Logic, through Church and Turing’s work, and the theory of “types” in Computer Science, which now plagues every Java code monkey, came from the “types” of Russell and Whithead’s heroic, and tragic, Principia Mathematica. So it is not surprising, historically speaking, that a certain type of computer scientist, or a certain kind of functional programmer, thinks that Homotopy Type Theory, which the previous link indicates is the “internal language of higher toposes” (whatever that means), is going to lead to to progress in software engineering.

I have never learned what a Type in Computer Science is. (I did write a compiler in Standard ML once, so it is not that I have never heard of the thing.) As far as I understand, it is not quite a formal concept. I long thought that the popularity of functional programming languages with highly complex type systems was just a computer science fad, a way for smart programmers to look cooler than the programmers around them. Eventually, however, it was explained to me that if you write code that creates the lithography for a microprocessor, and the resulting microprocessor has a bug, then you have to make a new microprocessor. Making a microprocessor is a multi-million dollar endeavor. So if hardcore type theory leads to fewer bugs, then it is manifestly worth it. The only reason, it would seem, that such tools are not used everywhere else, is because the correctness of most software simply does not matter enough.

Recently a friend of mine asked me to take her copy of the Homotopy Type Theory book. She in turn recieved it from a computer-science friend, who asserted that it is, in short, an earth-shattering work of staggering genius. I refused to take the book, because I have enough work to do, because I’ve never heard of someone using homotopy type theory to make the proof of a “trivial”, un-provable statement in higher category theory easy, and because I don’t need 281 pages to learn about the Hopf fibration.

In other words, I didn’t take it because I don’t know what HTT is and I’m not curious enough – a fault. But I have heard of some slogans about HTT, which brings me to the title of the post.

Here is a slogan for Homotopy Type Theory:

Think of mathematical statements as points. An implication $A \Rightarrow B$ is a path from $A$ to $B$. To demonstrate an implication one must give a proof of the implication; this is a choice. So one can ask: when are two proofs equivalent? One can give a proof that two proofs are equivalent, in a logical system that allows us to reason about proofs; this is a path between paths. Then one can ask whether the proof that the proofs are equivalent proves any other equivalences between proofs; such higher proofs are paths between paths between paths…

From this perspective, mathematics is simply the study of some “specific” $(\infty, \infty)$-category, or $\omega$-category, which I will call $Mathematics$. Neither this category, nor the theory of such categories, has a formalization. We reward mathematicians for finding new proofs; for finding new paths between $A$ and $B$. These contribute to the fundamental group of $Mathematics$. But giving a proof isn’t enough, and we want to understand how different proofs are related, so we find proofs that formalize analogies between proofs, and give proofs that different proofs are morally equivalent; these contribute to paths between paths, and kill lower-homotopy groups while creating higher-homotopy groups. Mathematics is a (slow, desparate) race to compute the homotopy type of $Mathematics$. Thus, a

Conjecture: The homotopy type of $Mathematics$ is the homotopy type of a point.

Any two proofs are related by an analogy; any two implications are related from the right perspective. Of course, maybe this is false. But one wonders!