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:
- 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).
- Type theorists are seeing topology as a way to get new insights on type theory and variants thereof.
- 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?