# Homotopy Type Theory: What is it?

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?

## migrated from math.stackexchange.comMar 18 '15 at 19:25

This question came from our site for people studying math at any level and professionals in related fields.

• there have been some popular surveys, including in the AMS Notices I think, available online. – Will Jagy Mar 18 '15 at 0:57
• @WillJagy This thing ams.org/notices/201309/rnoti-p1164.pdf ? – James Mar 18 '15 at 1:00
• Maybe. I believe I was thinking of one of their tiny "what is?" columns, but this will do. I'm just relying on memory here, and not on a topic in which I have any involvement. – Will Jagy Mar 18 '15 at 1:03
• The canonical references are the HoTT blog at homotopytypetheory.org and the textbook they published (available for free via that site). – Ptharien's Flame Mar 18 '15 at 17:16
• While not specifically about HoTT, Mike Shulman's blog post golem.ph.utexas.edu/category/2013/01/… is worth reading. It cleared some things up for me, in response to my comment on his answer below. – Iian Smythe Mar 19 '15 at 15:33

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.

• Could you say more about how "it more closely matches mathematical practice", in comparison to set theory? From a naive perspective, it seems like there would be many objects in mathematics that are just as painful to encode in this formalism as others are in set theory; they just might be different objects. – Iian Smythe Mar 18 '15 at 19:42
• @iian: As someone who doesn't really understand this stuff, I think that point is not about how "painful" something is, but a move away from the practice of putting lots of extra irrelevant information into the coding. e.g. away from having to do things like $(a,b)$ to be the specific set $\{\{a\}, \{a,b\}\}$, which contains a lot of information it really shouldn't -- e.g. for every set $X$, the expression $X \in (a,b)$ has a meaningful value. – Hurkyl Mar 18 '15 at 20:46
• @IianSmythe I wrote a whole blog post about this: golem.ph.utexas.edu/category/2013/01/… – Mike Shulman Mar 19 '15 at 3:15
• @IianSmythe, in the same vein as Hurkyl's comment, Set theory allows you to ask whether pi (defined as you wish, coded as a set, respecting strictly the pseudo a conventions we are used to) is a group. Or whether 3 is a topology (it is...). – ACL Mar 19 '15 at 8:37
• @IianSmythe I take it you are asking whether UF can prove that "UF, if consistent, does not prove or disprove CH" (analogously to how ZFC proves the analogous statement about itself). Answering this properly would take far more than 600 characters, but I think the short answer is "yes in an unsatisfying way; a more satisfactory way is part of an open research problem". The unsatisfying way is that inside UF we can build models of itself using the internal models of ZFC. The more satisfactory way would depend on solving homotopytypetheory.org/2014/03/03/hott-should-eat-itself. – Mike Shulman Mar 19 '15 at 17:31