In the introduction section of the "Homotopy Type Theory" (https://homotopytypetheory.org/book/) it is said that:

One problem in understanding type theory from a mathematical point of view, however, has always been that the basic concept of type is unlike that of set in ways that have been hard to make precise. We believe that the new idea of regarding types, not as strange sets (perhaps constructed without using classical logic), but as spaces, viewed from the perspective of homotopy theory, is a significant step forward.

But wouldn't it be circular to use the HoTT as the foundation of mathematics because we have already used the mathematical spaces to define the notion of "type"?


1 Answer 1


Types are not defined as spaces: if you take a type theory (such as HoTT) as your foundation, then types are a primitive notion, just like how sets are if you take some sort of set theory (such as ZFC, ETCS etc.) as your foundation.

You can of course model types as spaces, which is what Voevodsky did, and which led to the homotopy-theoretic interpretation of type theory.

  • 1
    $\begingroup$ What does it mean to "model types as spaces"? $\endgroup$
    – user56834
    Commented Dec 31, 2020 at 5:46
  • $\begingroup$ Here's an nLab article on the topic. $\endgroup$
    – ಠ_ಠ
    Commented Dec 31, 2020 at 12:49
  • $\begingroup$ Unfortunately the article is a bit beyond me (topoi, and so forth) $\endgroup$
    – user56834
    Commented Dec 31, 2020 at 14:05
  • $\begingroup$ I aksed this as a separate question here: math.stackexchange.com/questions/3967700/… $\endgroup$
    – user56834
    Commented Dec 31, 2020 at 14:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .