What is homotopy type theory? An amateur speaks.

Over the past few months I have been attempting to get some kind of an idea about what homotopy type theory is. Lean uses dependent type theory, which is another kind of type theory; homotopy type theory is what Voevodsky studied and what many other people still study. But Reid Barton made some comments on the Lean chat which basically opened my eyes and I’ll just write them down now before I forget them.

Last summer, a bunch of Imperial students formalised a bunch of mathematics in Lean. Most of them stuck to stuff on our undergraduate syllabus, but Ali Sever raised the possibility of “formalising Euclid” and even though at the time I had no real idea about how that would work, I said “sure”. It turns out that Ali was not the first person to think of this idea in the 2000+ years since the Elements was written, and things were very well-understood. But not by me. So here’s an explanation.

I used to have to deal with geometry problems when I was younger and found myself doing various Maths Olympiad problems. My gut feeling with the plane geometry problems was that “one should be able to do them all in theory just by working out the coordinates of everything”. However of course there were often very cute proofs which just involved invoking standard theorems in plane geometry (of which there seem to be very many, some of which are of course proved in Euclid’s books). Are these methods actually fundamentally different? They certainly look fundamentally different. In fact they must be fundamentally different, because Descartes didn’t invent Cartesian coordinates until over 1500 years after Euclid had died.

So synthetic geometry is what Euclid was doing; he never chose coordinates. He had an abstract notion of a point, and an abstract notion of a line, and axiomatised what he needed from them: between two distinct points one could draw a line, and so on. He never attempted to define “point” or “line” — for Euclid, these notions were fundamental and needed no definition [note added later on: David Corfield points out that actually Euclid did offer “definitions” of some sort for point and line, but arguably never then uses them]

On the other hand, analytic geometry is what you get if you use coordinates. We need the real numbers $\mathbb{R}$ (which we could have built using the axioms of our system) and then we can define the plane to be $\mathbb{R}^2$ and we can define a point to be an element of $\mathbb{R}^2$ (that is, a pair of real numbers), and we can define a line to be the subset of $\mathbb{R}^2$ defined by a degree 1 equation, and so on.

You can see that these are somehow two different theories. A powerful way of seeing this is that Euclid develops some geometry without assuming the parallel postulate, and then he assumes it and proves more. There was some sort of industry pre 1800 of trying to prove the parallel postulate from Euclid’s other axioms, but nobody was successful. Nowadays we understand why — all of Euclid’s axioms other than the parallel postulate hold for geometry done on a sphere (and the parallel postulate fails). As a consequence, all the results in planar geometry which Euclid proved without assuming the parallel postulate also hold for spherical geometry.

Tarski’s synthetic approach to geometry has an axiom (schema) of continuity, corresponding essentially to the completeness of the real numbers. It would not surprise me if the results that Tarski proved which did not assume completeness of the reals were also true in models of planar geometry such as $k^2$ where $k$ is an appropriate subfield of the reals (for example the real algebraic numbers, which are not complete).

What we begin to see is that with the synthetic approach, we are inspired by the particular picture we’re trying to model, but there might be other models too, and we might have to add other axioms later on for convenience if we want to prove more results about the particular model we have in mind (and indeed we will have to add these axioms if there are other models of our theory in which these results are false).

In mathematics, we can define topological spaces, and talk about maps between them, and what it means for maps to be homotopic, and then invent homotopy theory, the basics of which are taught to second year maths undergraduates at Imperial College if they choose this option. One could regard this as “analytic homotopy theory”.

What homotopy type theory is, I now finally realise, is a synthetic version of this. There are types `X : Type` and then there are terms `a : X` . The model is that `X` is supposed to be a topological space, and `a` is supposed to be an element of `X`. But here’s the weird part. The equation `a = b` is not supposed to be interpreted as meaning that the points `a` and `b` are equal. A proof of `a = b` (or, to give it its more formal name, a term of type `a = b`) is supposed to be interpreted as a path from `a` to `b`. Symmetry of equality is then interpreted as saying that if we have a path from `a` to `b` then we have a path from `b` to `a`, and transitivity is just path composition. If we have two terms `p1` and `p2` of type `a = b` then a term of type `p1 = p2` is a path from `p1` to `p2`, or, in other words, a homotopy between `p1` and `p2`. I had read this interpretation several times, and have known full well for over a year that this is how I was supposed to “interpret equality” — but the penny had never dropped as to what that actually even meant. But now I get it, or at least the basic idea:

Homotopy type theory is to the theory of topological spaces and homotopy classes of maps, as Euclid’s synthetic geometry is to Descartes’ coordinate geometry.

I read in Floris van Doorn’s thesis that it is an open problem to define Grassmannians in homotopy type theory. When I first read this, I was completely confused. One can build mathematics in homotopy type theory, so one can build topological spaces, the real numbers, and build Grassmannians the way they are usually built in a maths course. It was Reid Barton who pointed out to me that this was not what the question meant. Of course one can do this — this would be an analytic construction. The open problem is to give a synthetic construction. It is analogous to me saying that one could just prove an olympiad geometry question by a coordinate chase. I am clearly an unsynthetic kind of guy. Of course, one issue could be that there are perhaps other models of the axioms of homotopy type theory where Grassmannians really don’t exist…

Thanks to Ali Sever, whose questions and research last summer turned out to be a necessary prerequisite for the penny to drop. Ali’s work formalising Tarski’s synthetic geometry in Lean is here.

The Xena Project aims to get mathematics undergraduates (at Imperial College and beyond) trained in the art of formalising mathematics on a computer. Why? Because I have this feeling that digitising mathematics will be really important one day.
This entry was posted in undergrad maths and tagged , , , , , , . Bookmark the permalink.

12 Responses to What is homotopy type theory? An amateur speaks.

1. David Corfield says:

“He never attempted to define “point” or “line” — for Euclid, these notions were fundamental and needed no definition.”

Well, strictly that’s not right, see https://mathcs.clarku.edu/~djoyce/java/elements/bookI/bookI.html#defs. But you could say he doesn’t use them.

Like

2. Charles Rezk says:

I would be better to say that: “A proof of a = b (or, to give it its more formal name, a term of type a = b) is supposed to be interpreted as *a choice of path* from a to b”, rather than “a homotopy class of paths”.

Like

• xenaproject says:

Oh! So this sounds like something I should actually fix. A term of type a=b is a choice of path, and if I have two terms h1 and h2 of type a=b then a proof that h1 = h2 is a homotopy of paths. Have I got this straight now?

Like

• xenaproject says:

Post updated. Thanks for pointing this out. I did put a warning in the title 😉

Like

• rezkc says:

Sounds good.

Like

3. David Hansen says:

So what happened in Paris?

Like

• xenaproject says:

Ha ha. We were talking to a room full of philosophers and historians. So Michael Harris told everyone that nothing he writes in any of his papers should be thought of as a theorem, what he writes is just ideas, like a kind of story. I gave examples of holes in mathematics (e.g. I talked about the 100 page hole in the appendix of the Gaitsgory-Rosenblyum book) and said how 100 page holes were fine, kind of, and then Patrick Massot showed them how cool filters were in Lean. And then we all went off to drink wine and eat cheese and they asked us questions. It was all extremely civil and I was very pleased to have gone. For me one interesting thing was meeting David Rabouin, a historian who claimed that mathematics has been constantly full of holes for centuries, and I was deluded in thinking that the fact that 100 years ago we wrote down some axioms changes anything.

Like

• David Hansen says:

Thanks for the information! Which 100 page hole is this more specifically?

By the way, have you heard of Almgren’s Big Regularity Paper? If not, I suggest you look it up.

Like

• xenaproject says:

http://www.math.harvard.edu/~gaitsgde/GL/Basics.pdf section 0.4, just general abstract nonsense which is missing from the literature. In maths this is fine. In computer science this literature would “not compile”. It’s an interesting question as to which of my papers would compile. Of course the answer can change over time, but it can only increase.

Like

4. Anon says:

“Nowadays we understand why — all of Euclid’s axioms other than the parallel postulate hold for geometry done on a sphere (and the parallel postulate fails).”

Euclid’s first postulate is typically interpreted to mean that there exists a *unique* line through any two distinct points. Spherical geometry does not satisfy this axiom (lots of great circles through antipodal points). Mathematicians trying to prove the parallel postulate would have been well aware of spherical geometry and which axioms it did and did not satisfy. It was the discovery of *hyperbolic geometry* that led them to abandon their search.

Like

5. xenaproject says:

I told you I was an amateur! Many thanks for this observation!

Like