A meaning explanation for HoTT.
In the Univalent Foundations of mathematics spatial notions like "point" and "path" are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Ho...
| Publicado en: | Synthese Vol. 197; no. 2; pp. 651 - 681 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Springer Nature
Feb2020
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| Sumario: | In the Univalent Foundations of mathematics spatial notions like "point" and "path" are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory (as a formalism for the Univalent Foundations) can be justified intuitively as a theory of shapes in the same way that ZFC (as a formalism for set-theoretic foundations) can be justified intuitively as a theory of collections. I first clarify what such an "intuitive justification" should be by distinguishing between formal and pre-formal "meaning explanations" in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like "shape", "path" etc. |
|---|