## Abstract

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.

## Keywords

Meaning explanation Homotopy type theory Univalent foundations Set theory## Notes

### Acknowledgements

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).

## References

- 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 - Altenkirch, T., & McBride, C. (2006). Towards observational type theory. Manuscript, available online.Google Scholar
- Angiuli, C., Harper, R., & Wilson, T. (2016). Computational higher type theory I: Abstract cubical realizability. arXiv preprint arXiv:1604.08873
- Awodey, S. (2014). Structuralism, Invariance and univalence.
*Philosophia Mathematica*,*22*(1), 1–11.CrossRefGoogle Scholar - 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 - 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 - Boolos, G. (1971). The iterative conception of set.
*The Journal of Philosophy*,*68*(8), 215–231.CrossRefGoogle Scholar - Burgess, J. (2014).
*Rigor and structure*. Oxford: Oxford University Press.Google Scholar - Cartmell, J. (1986). Generalized algebraic theories and contextual categories.
*Annals of Pure and Applied Logic*,*32*, 209–243.CrossRefGoogle Scholar - 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
- Corfield, D. (2015). Reviving the philosophy of geometry. http://philsci-archive.pitt.edu/11809/
- Corfield, D. (2016). Expressing “the structure of” in homotopy type theory. http://philsci-archive.pitt.edu/11862/
- Dybjer, P. (2012). Program testing and the meaning explanations of intuitionistic type theory. Available at http://www.cse.chalmers.se/~peterd/papers/MartinLofFestschrift.pdf
- 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 - Grayson, D. (2017). An introduction to the univalent foundations for mathematicians. arXiv preprint. Available at https://arxiv.org/pdf/1711.01994.pdf
- Hellman, G., & Shapiro, S. (2013). The classical continuum without points.
*Review of Symbolic Logic*,*6*(3), 488–512.CrossRefGoogle Scholar - Hou, K. B. (2017). Higher-dimensional types in the mechanization of homotopy theory. Ph.D. thesis, CMU.Google Scholar
- Kapulkin, K., Lumsdaine, P., & Voevodsky, V. (2014). The simplicial model of univalent foundations. arXiv:1211.2851v2
- Ladyman, J., & Presnell, S. (2015). Identity in homotopy type theory, Part I: The justification of path induction. Philosophia Mathematica.Google Scholar
- Lawvere, W. (2005). An elementary theory of the category of sets.
*Reprints in Theory and Applications of Categories*,*12*, 1–35.Google Scholar - Linnebo, Ø., & Pettigrew, R. (2011). Category theory as an autonomous foundation.
*Philosophia Mathematica*, pp. 1–30.Google Scholar - Marquis, J. P. (2013). Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics.
*Synthese*,*190*(12), 2141–2164.CrossRefGoogle Scholar - Martin-Löf, P. (1982). Constructive mathematics and computer programming.
*Studies in Logic and the Foundations of Mathematics*,*104*, 153–175.CrossRefGoogle Scholar - Martin-Löf, P. (1984).
*Intuitionistic type theory*. Bibliopolis.Google Scholar - Martin-Löf, P. (1987). Truth of a proposition, evidence of a judgement, validity of a proof.
*Synthese*,*73*, 407–420.CrossRefGoogle Scholar - 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 - Pelayo, Á., & Warren, M. (2014). Homotopy type theory and Voevodsky’s univalent foundations.
*Bulletin of the American Mathematical Society*,*51*(4), 597–648.CrossRefGoogle Scholar - Rodin, A. (2014). On constructive axiomatic method. Available at http://philsci-archive.pitt.edu/10986/
- Shulman, M. (2016). Homotopy type theory: A synthetic approach to higher equalities. In E. Landry (Ed.)
*Categories for the working philosopher*.Google Scholar - Tsementzis, D. (2016). First-order logic with isomorphism. arXiv preprint arXiv:1603.03092
- Tsementzis, D. (2016). Univalent foundations as structuralist foundations.
*Synthese*, pp. 1–35. https://doi.org/10.1007/s11229-016-1109-x. - Tsementzis, D. (2017). What is a higher-level set?
*Philosophia Mathematica*. https://doi.org/10.1093/philmat/nkw032 - Tsementzis, D., & Halvorson, H. (2017). Foundations and philosophy. Philosopher’s Imprint. http://philsci-archive.pitt.edu/13504/. Forthcoming
- Univalent foundations program: Homotopy type theory: Univalent foundations of mathematics (2013). http://homotopytypetheory.org/book
- Voevodsky, V. (2006). Foundations of mathematics and homotopy theory. https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VV%20Slides.pdf
- Voevodsky, V. (2010). The equivalence axiom and univalent models of type theory. Talk at CMU.Google Scholar
- Voevodsky, V. (2010). Univalent foundations project. http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf
- Voevodsky, V. (2014). Subsystems and regular quotients of C-systems. arXiv:1406.5389, submitted pp. 1–11. arXiv:1406.7413
- Voevodsky, V. (2014). Univalent foundations (lecture at the IAS). https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_IAS.pdf
- Voevodsky, V., Ahrens, B., & Grayson, D., et al. (2017).
*UniMath*: Univalent mathematics. Available at https://github.com/UniMath - Warren, M. A. (2008). Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University.Google Scholar