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"?


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.