Homotopy Type Theory: What is it?

Question

My question is, broadly, what is the main project of Homotopy Type Theory (HoTT). I asked a professor who is likely to be correct and he say the following:

There are three directions:

1. Topologists are seeing type theory as a concise and convenient ways to reason about topology, where equalities are interpreted as paths (and higher-dimensional variants thereof).
2. Type theorists are seeing topology as a way to get new insights on type theory and variants thereof.
3. People are pushing univalence and constructive type theory as a new foundations for mathematics.

The only one of those I have any grip on is 2. My understanding, gleaned from some talks I didn't understand goes like this:

Some people would like to write a proof checking/generating client that is sufficiently expressive so that you can actually do mathematics in it. The way that they get this high level of expressiveness is through a very rich type theory.

It was noticed that you could intepret these types topologically: An object is a point, a proof of equality is a path, a proof that two proofs of equality are "the same" is a homotopy.

Now, people use attractive features of the model, to guide further development of the proof environment, which is approximately point 2.

Somehow though, there is a hope that you can use this system to compute homotopy groups of spheres? Why is this credible?

Also, this is being pushed as a new foundation? Why? What advantages does it have over set theory?

Answer 1

That description of the three directions is not too bad, although they are not of course completely separate, nor does everything called HoTT fall under one of them. Also, I'm not sure whether this applies to you, but I always point out that it is potentially confusing to say "topology" when what is meant is "homotopy theory", i.e. "$\infty$-groupoid theory" — all "spaces" appear in HoTT only up to homotopy.

Some people would like to write a proof checking/generating client that is sufficiently expressive so that you can actually do mathematics in it.

I'm not sure what use a proof checking program would be if you couldn't do mathematics in it... (-:

But yes, I think your description of point 2 is roughly accurate. Point 1 is just about using the model in the other direction: if you prove something in the type theory, then it's true as a statement about spaces. In particular, if you calculate something like a homotopy group of a sphere in the type theory, then it's also a true statement about the homotopy groups of spheres in classical algebraic topology. And in fact we've done this in a few simple cases, like $\pi_n(S^n)$ and $\pi_3(S^2)$, so it better ought to be credible. These proofs are different from the classical ones, elegant in a certain sense, and relatively easily formalizable in a proof assistant. (Notice that I'm talking about different proofs of known results here; it's not inconceivable that the new methods of HoTT might lead to proofs of new results even in classical homotopy theory, but I expect that day is far in the future.)

As for point 3, type theory in general has a lot of advantages over set theory as a foundation for mathematics. Among other things, it requires less arbitrary "encoding" to represent math, it more closely matches mathematical practice, and it can be more easily programmed in a computer, producing small "proof term" certificates that can be easily verified. UF/HoTT potentially fixes some of the disadvantages of traditional type theory, such as a lack of well-behaved quotients and the problem of transporting structures across equivalences, so it's even better. And in addition to traditional mathematics, it also includes new mathematics such as the "synthetic homotopy theory" calculations of homotopy groups mentioned above.

Finally, a point that I always emphasize: HoTT has many models other than the "standard" one in spaces. Roughly we can use any "$(\infty,1)$-topos" (although there are coherence questions still work in progress). This means that when we prove something in UF/HoTT (such as a homotopy group calculation, or any part of traditional mathematics that we might formalize using it as a foundation) the result is more general than in classical homotopy theory, since it is true in any of the models.