In Homotopy Type Theory (HoTT in what follows) one may compute homotopy groups of objects that bear names that are the same as some usual spaces: for instance one may consider $S^1$ which is defined by $*:S^1, b : *=_{S^1}*$ and with the usual induction principle, and compute its homotopy groups.
It has been proved for instance that with this definition $\pi_1(S^1) = \mathbb{Z}$ and the higher homotopy groups vanish, which coincides with the usual homotopy groups of the usual $S^1$.
Now it seems that all the homotopy groups that have been computed in HoTT so far (say of spheres) coincide with the usual ones (in the sense that they have the same description : we can't literally compare them because they don't live in the same theory). My question is : how much of it is a coincidence ? I expect that it's not a coincidence, and so my real question is actually : can we explain it ? If so, in what terms ?
I'm not asking for a proof, but my problem is, the result seems even hard to state (as I said : the groups are not living in the same theory, and to begin how do we even relate HoTT's $S^1$ with the usual $S^1$ ? ).
So I would want an answer that explains how to state the result (not necessarily the details, but at least the main ideas), and how to prove it (again, the main ideas of proof – I expect something like "oh so we have this model of HoTT that we can define in set theory, and when you interpret HoTT in this model, $S^1$ looks like the circle and its homotopy groups look like the usual homotopy groups")
Best Answer
All homotopy groups that can be computed in HoTT coincide with the corresponding classical homotopy groups. This is because HoTT has an interpretation in the Quillen model category of simplicial sets (constructed in a metatheory of ZFC plus some inaccessible cardinals, although probably a much weaker theory suffices), constructed by Voevodsky, which is also Quillen equivalent to classical homotopy theory. Thus, any calculation in HoTT can be interpreted into simplicial sets and then transferred across that equivalence to classical homotopy theory.
A much more interesting (and open!) question is whether every computation of a classical homotopy group is also provable in HoTT. This is interesting and nontrivial because the really interesting thing about HoTT (from my point of view) is that it also has lots of other models, namely in all higher toposes. Thus, this question is tantamount to asking whether the homotopy groups of spheres (say) are the same in all higher toposes.
(Technical fine print: we know by an extrinsic argument that the homotopy groups of spheres and other finite complexes are the same in all "Grothendieck" higher toposes, but there are also other models, and reasoning about any particular class of models can't answer the question of what can be proven internally in HoTT.)