pp 1–30 | Cite as

A meaning explanation for HoTT

  • Dimitris TsementzisEmail author
S.I.: Foundations of Mathematics


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.


Meaning explanation Homotopy type theory Univalent foundations Set theory 



I would like to thank John Burgess, Harvey Friedman, Hans Halvorson, Bob Harper, and Colin McLarty for many helpful comments on several earlier drafts. I would also like to single out in thanks Harry Crane, both for his many insightful comments and questions on the many earlier versions of this paper, as well as for his encouragement and support. Finally, I would like to thank two anonymous referees for highly engaged and illuminating remarks that led to many substantial improvements to the paper. This work was partially supported by NSF CAREER-DMS-1554092 (P.I. Harry Crane).


  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.Google Scholar
  2. Altenkirch, T., & McBride, C. (2006). Towards observational type theory. Manuscript, available online.Google Scholar
  3. Angiuli, C., Harper, R., & Wilson, T. (2016). Computational higher type theory I: Abstract cubical realizability. arXiv preprint arXiv:1604.08873
  4. Awodey, S. (2014). Structuralism, Invariance and univalence. Philosophia Mathematica, 22(1), 1–11.CrossRefGoogle Scholar
  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.Google Scholar
  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.Google Scholar
  7. Boolos, G. (1971). The iterative conception of set. The Journal of Philosophy, 68(8), 215–231.CrossRefGoogle Scholar
  8. Burgess, J. (2014). Rigor and structure. Oxford: Oxford University Press.Google Scholar
  9. Cartmell, J. (1986). Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32, 209–243.CrossRefGoogle Scholar
  10. Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2015). Cubical type theory: A constructive interpretation of the univalence axiom.
  11. Corfield, D. (2015). Reviving the philosophy of geometry.
  12. Corfield, D. (2016). Expressing “the structure of” in homotopy type theory.
  13. Dybjer, P. (2012). Program testing and the meaning explanations of intuitionistic type theory. Available at
  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).Google Scholar
  15. Grayson, D. (2017). An introduction to the univalent foundations for mathematicians. arXiv preprint. Available at
  16. Hellman, G., & Shapiro, S. (2013). The classical continuum without points. Review of Symbolic Logic, 6(3), 488–512.CrossRefGoogle Scholar
  17. Hou, K. B. (2017). Higher-dimensional types in the mechanization of homotopy theory. Ph.D. thesis, CMU.Google Scholar
  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.Google Scholar
  20. Lawvere, W. (2005). An elementary theory of the category of sets. Reprints in Theory and Applications of Categories, 12, 1–35.Google Scholar
  21. Linnebo, Ø., & Pettigrew, R. (2011). Category theory as an autonomous foundation. Philosophia Mathematica, pp. 1–30.Google Scholar
  22. Marquis, J. P. (2013). Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics. Synthese, 190(12), 2141–2164.CrossRefGoogle Scholar
  23. Martin-Löf, P. (1982). Constructive mathematics and computer programming. Studies in Logic and the Foundations of Mathematics, 104, 153–175.CrossRefGoogle Scholar
  24. Martin-Löf, P. (1984). Intuitionistic type theory. Bibliopolis.Google Scholar
  25. Martin-Löf, P. (1987). Truth of a proposition, evidence of a judgement, validity of a proof. Synthese, 73, 407–420.CrossRefGoogle Scholar
  26. Martin-Löf, P. (1996). On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1(1), 11–60.Google Scholar
  27. Pelayo, Á., & Warren, M. (2014). Homotopy type theory and Voevodsky’s univalent foundations. Bulletin of the American Mathematical Society, 51(4), 597–648.CrossRefGoogle Scholar
  28. Rodin, A. (2014). On constructive axiomatic method. Available at
  29. Shulman, M. (2016). Homotopy type theory: A synthetic approach to higher equalities. In E. Landry (Ed.) Categories for the working philosopher.Google Scholar
  30. Tsementzis, D. (2016). First-order logic with isomorphism. arXiv preprint arXiv:1603.03092
  31. Tsementzis, D. (2016). Univalent foundations as structuralist foundations. Synthese, pp. 1–35.
  32. Tsementzis, D. (2017). What is a higher-level set? Philosophia Mathematica.
  33. Tsementzis, D., & Halvorson, H. (2017). Foundations and philosophy. Philosopher’s Imprint. Forthcoming
  34. Univalent foundations program: Homotopy type theory: Univalent foundations of mathematics (2013).
  35. Voevodsky, V. (2006). Foundations of mathematics and homotopy theory.
  36. Voevodsky, V. (2010). The equivalence axiom and univalent models of type theory. Talk at CMU.Google Scholar
  37. Voevodsky, V. (2010). Univalent foundations project.
  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).
  40. Voevodsky, V., Ahrens, B., & Grayson, D., et al. (2017). UniMath: Univalent mathematics. Available at
  41. Warren, M. A. (2008). Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University.Google Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.BrooklynUSA

Personalised recommendations