×
Tsementzis, Dimitris

A meaning explanation for HoTT. (English) Zbl 1475.03055

Synthese 197, No. 2, 651-680 (2020).
Summary: 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.

MSC:

03A05 Philosophical and critical aspects of logic and foundations
03B38 Type theory
55U35 Abstract and axiomatic homotopy theory in algebraic topology

Keywords:

meaning explanation; homotopy type theory; univalent foundations; set theory

Software:

cubicaltt; GitHub; UniMath
PDF BibTeX XML Cite
\textit{D. Tsementzis}, Synthese 197, No. 2, 651--680 (2020; Zbl 1475.03055)
Full Text: DOI Link
  • logo of hbz
  • logo of WorldCat

References:

[1] Aczel, P. (1978). The type theoretic interpretation of constructive set theory. In L. P. A. MacIntrye & J. Paris (Eds.), Logic colloquium ’77 (Proc. Conf., Wroclaw, 1977), Stud. Logic Foundations Math. (vol. 96, pp. 55-66). Amsterdam, New York: North-Holland. · Zbl 0481.03035
[2] Altenkirch, T., & McBride, C. (2006). Towards observational type theory. Manuscript, available online.
[3] Angiuli, C., Harper, R., & Wilson, T. (2016). Computational higher type theory I: Abstract cubical realizability. arXiv preprint arXiv:1604.08873
[4] Awodey, S., Structuralism, Invariance and univalence, Philosophia Mathematica, 22, 1, 1-11 (2014) · Zbl 1310.03021
[5] Awodey, S., & Warren, M. A. (2009). Homotopy theoretic models of identity types. In Mathematical proceedings of the Cambridge Philosophical Society, vol. 146, no 45, pp. 45-55. · Zbl 1205.03065
[6] Bezem, M., Coquand, T., & Huber, S. (2014). A model of type theory in cubical sets. In 19th International conference on types for proofs and programs (TYPES 2013), vol. 26, pp. 107-128. · Zbl 1359.03009
[7] Boolos, G., The iterative conception of set, The Journal of Philosophy, 68, 8, 215-231 (1971)
[8] Burgess, J., Rigor and structure (2014), Oxford: Oxford University Press, Oxford
[9] Cartmell, J., Generalized algebraic theories and contextual categories, Annals of Pure and Applied Logic, 32, 209-243 (1986) · Zbl 0634.18003
[10] Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2015). Cubical type theory: A constructive interpretation of the univalence axiom. https://www.math.ias.edu/ amortberg/papers/cubicaltt.pdf · Zbl 1434.03036
[11] Corfield, D. (2015). Reviving the philosophy of geometry. http://philsci-archive.pitt.edu/11809/
[12] Corfield, D. (2016). Expressing “the structure of” in homotopy type theory. http://philsci-archive.pitt.edu/11862/
[13] Dybjer, P. (2012). Program testing and the meaning explanations of intuitionistic type theory. Available at http://www.cse.chalmers.se/ peterd/papers/MartinLofFestschrift.pdf · Zbl 1314.03032
[14] Gelfand, M. (2009). We do not choose mathematics as our profession, it chooses us: Interview with Yuri Manin. Notices of the AMS, 56(10). · Zbl 1178.01044
[15] Grayson, D. (2017). An introduction to the univalent foundations for mathematicians. arXiv preprint. Available at https://arxiv.org/pdf/1711.01994.pdf · Zbl 1461.03012
[16] Hellman, G.; Shapiro, S., The classical continuum without points, Review of Symbolic Logic, 6, 3, 488-512 (2013) · Zbl 1326.03019
[17] Hou, K. B. (2017). Higher-dimensional types in the mechanization of homotopy theory. Ph.D. thesis, CMU.
[18] Kapulkin, K., Lumsdaine, P., & Voevodsky, V. (2014). The simplicial model of univalent foundations. arXiv:1211.2851v2
[19] Ladyman, J., & Presnell, S. (2015). Identity in homotopy type theory, Part I: The justification of path induction. Philosophia Mathematica. · Zbl 1380.03027
[20] Lawvere, W., An elementary theory of the category of sets, Reprints in Theory and Applications of Categories, 12, 1-35 (2005) · Zbl 1072.18005
[21] Linnebo, Ø., & Pettigrew, R. (2011). Category theory as an autonomous foundation. Philosophia Mathematica, pp. 1-30. · Zbl 1270.18001
[22] Marquis, Jp, Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics, Synthese, 190, 12, 2141-2164 (2013) · Zbl 1284.00042
[23] Martin-Löf, P., Constructive mathematics and computer programming, Studies in Logic and the Foundations of Mathematics, 104, 153-175 (1982) · Zbl 0541.03034
[24] Martin-Löf, P. (1984). Intuitionistic type theory. Bibliopolis. · Zbl 0571.03030
[25] Martin-Löf, P., Truth of a proposition, evidence of a judgement, validity of a proof, Synthese, 73, 407-420 (1987)
[26] Martin-Löf, P., On the meanings of the logical constants and the justifications of the logical laws, Nordic Journal of Philosophical Logic, 1, 1, 11-60 (1996) · Zbl 0885.03009
[27] Pelayo, Á.; Warren, M., Homotopy type theory and Voevodsky’s univalent foundations, Bulletin of the American Mathematical Society, 51, 4, 597-648 (2014) · Zbl 1432.03019
[28] Rodin, A. (2014). On constructive axiomatic method. Available at http://philsci-archive.pitt.edu/10986/ · Zbl 1436.03314
[29] Shulman, M. (2016). Homotopy type theory: A synthetic approach to higher equalities. In E. Landry (Ed.) Categories for the working philosopher.
[30] Tsementzis, D. (2016). First-order logic with isomorphism. arXiv preprint arXiv:1603.03092
[31] Tsementzis, Dimitris, Univalent foundations as structuralist foundations, Synthese, 194, 9, 3583-3617 (2016) · Zbl 1400.03023
[32] Tsementzis, D. (2017). What is a higher-level set? Philosophia Mathematica. 10.1093/philmat/nkw032
[33] Tsementzis, D., & Halvorson, H. (2017). Foundations and philosophy. Philosopher’s Imprint. http://philsci-archive.pitt.edu/13504/. Forthcoming
[34] Univalent foundations program: Homotopy type theory: Univalent foundations of mathematics (2013). http://homotopytypetheory.org/book · Zbl 1298.03002
[35] Voevodsky, V. (2006). Foundations of mathematics and homotopy theory. https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VV
[36] Voevodsky, V. (2010). The equivalence axiom and univalent models of type theory. Talk at CMU.
[37] Voevodsky, V. (2010). Univalent foundations project. http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf
[38] Voevodsky, V. (2014). Subsystems and regular quotients of C-systems. arXiv:1406.5389, submitted pp. 1-11. arXiv:1406.7413
[39] Voevodsky, V. (2014). Univalent foundations (lecture at the IAS). https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_IAS.pdf
[40] Voevodsky, V., Ahrens, B., & Grayson, D., et al. (2017). UniMath: Univalent mathematics. Available at https://github.com/UniMath
[41] Warren, M. A. (2008). Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.