Abstract
The intended model of the homotopy type theories used in Univalent Foundations is the ∞-category of homotopy types, also known as ∞-groupoids. The problem of higher structures is that of constructing the homotopy types needed for mathematics, especially those that aren’t sets. The current repertoire of constructions, including the usual type formers and higher inductive types, suffice for many but not all of these. We discuss the problematic cases, typically those involving an infinite hierarchy of coherence data such as semi-simplicial types, as well as the problem of developing the meta-theory of homotopy type theories in Univalent Foundations. We also discuss some proposed solutions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In Voevodsky (2014) he wrote: “The greatest roadblock for me was the idea that categories are ‘sets in the next dimension.’ I clearly recall the feeling of a breakthrough that I experienced when I understood that this idea is wrong. Categories are not ‘sets in the next dimension.’ They are ‘partially ordered sets in the next dimension’ and ‘sets in the next dimension’ are groupoids.”
- 2.
- 3.
- 4.
See https://ncatlab.org/homotopytypetheory/show/open+problems for an up-to-date list of open problems.
References
Ahrens, B., Kapulkin, K., & Shulman, M. (2015). Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25(5), 1010–1039. https://doi.org/10.1017/S0960129514000486
Altenkirch, T., & Kaposi, A. (2016). Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’16 (pp. 18–29). New York: ACM. https://doi.org/10.1145/2837614.2837638
Altenkirch, T., Capriotti, P., & Kraus, N. (2016). Extending homotopy type theory with strict equality. In Computer science logic 2016, LIPIcs. Leibniz International Proceedings in Informatics (Vol. 62, pp. Art. No. 21, 17). Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern.
Altenkirch, T., Danielsson, N. A., & Kraus, N. (2017). Partiality, revisited. In J. Esparza & A. S. Murawski (Eds.), Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, 22–29 Apr 2017, Proceedings (pp. 534–549). Berlin/Heidelberg: Springer. https://doi.org/10.1007/978-3-662-54458-7_31
Angiuli, C., Harper, R., & Wilson, T. (2017). Computational higher-dimensional type theory. In POPL’17: Proceedings of the 44th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 680–693). ACM. https://doi.org/10.1145/3009837.3009861
Angiuli, C., & Harper, R. (2018). Meaning explanations at higher dimension. Indagationes Mathematicae, 29(1), 135–149. https://doi.org/10.1016/j.indag.2017.07.010. L.E.J. Brouwer, fifty years later.
Annenkov, D., Capriotti, P., & Kraus, N. (2017). Two-level type theory and applications. https://arxiv.org/abs/1705.03307. Preprint.
Awodey, S. (2014). Structuralism, invariance, and univalence. Philosophia Mathematica (3), 22(1), 1–11. https://doi.org/10.1093/philmat/nkt030
Awodey, S. (2018). Univalence as a principle of logic. Indagationes Mathematicae. https://doi.org/10.1016/j.indag.2018.01.011
Baez, J. (2007). The homotopy hypothesis. http://math.ucr.edu/home/baez/homotopy/. Lecture at Higher Categories and Their Applications, Thematic Program on Geometric Applications of Homotopy Theory, Fields Institute, Toronto.
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), LIPIcs. Leibniz International Proceedings in Informatics (Vol. 26, pp. 107–128). Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern. https://doi.org/10.4230/LIPIcs.TYPES.2013.107
Boardman, J., & Vogt, R. (1973). Homotopy invariant algebraic structures on topological spaces (Vol. 347). Cham: Springer.
Brunerie, G. (2016). On the homotopy groups of spheres in homotopy type theory. Ph.D. thesis, Laboratoire J.A. Dieudonné. https://arxiv.org/abs/1606.05916
Buchholtz, U., & Morehouse, E. (2017). Varieties of cubical sets. In P. Höfner, D. Pous, & G. Struth (Eds.), RAMICS 2017: Relational and algebraic methods in computer science, Lecture notes in computer science (Vol. 10226). Cham: Springer. https://doi.org/10.1007/978-3-319-57418-9_5
Buchholtz, U., & Rijke, E. (2017). The real projective spaces in homotopy type theory. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) (pp. 1–8). New York: IEEE. https://doi.org/10.1109/LICS.2017.8005146
Buchholtz, U., & Favonia (Hou), K. B. (2018). Cellular cohomology in homotopy type theory. https://arxiv.org/abs/1802.02191. Accepted for Proceedings of Logic in Computer Science (LICS 2018).
Buchholtz, U., & Rijke, E. (2018). The Cayley-Dickson construction in homotopy type theory. To appear in Higher Structures.
Buchholtz, U., van Doorn, F., & Rijke, E. (2018). Higher groups in homotopy type theory. https://arxiv.org/abs/1802.04315. Accepted for Proceedings of Logic in Computer Science (LICS 2018).
Capriotti, P., & Kraus, N. (2017). Univalent higher categories via complete semi-Segal types. https://arxiv.org/abs/1707.03693. Preprint.
Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2018). Cubical type theory: A constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), LIPIcs. Leibniz International Proceedings in Informatics, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern. https://doi.org/10.4230/LIPIcs.TYPES.2015.5
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T., Smith, S. F. (1986). Implementing mathematics with the Nuprl proof development system. Prentice-Hall. http://www.nuprl.org/
Elmendorf, A., Kříž, I., Mandell, M. A., & May, J. (1995). Modern foundations for stable homotopy theory. In Handbook of algebraic topology (pp. 213–253). Amsterdam: North-Holland.
Grothendieck, A. (1983). Pursuing stacks. http://thescrivener.github.io/PursuingStacks/. Manuscript.
Harpaz, Y. (2015). Quasi-unital ∞-categories. Algebraic & Geometric Topology, 15(4), 2303–2381. https://doi.org/10.2140/agt.2015.15.2303
Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175(1–3), 207–222. https://doi.org/10.1016/S0022-4049(02)00135-4
Kan, D. M. (1956). Abstract homotopy. III. Proceedings of the National Academy of Sciences of the United States of America, 42, 419–421. https://doi.org/10.1073/pnas.42.7.419
Klein, F. (1872). Vergleichende Betrachtungen über neuere geometrische Forschungen. Verlag von Andreas Deichert, Erlangen.
Kraus, N. (2016). Constructions with non-recursive higher inductive types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS’16) (pp. 595–604). New York: ACM. https://doi.org/10.1145/2933575.2933586
Kraus, N., & Sattler, C. (2015). Higher homotopies in a hierarchy of univalent universes. ACM Transactions on Computational Logic, 16(2), 18:1–18:12. https://doi.org/10.1145/2729979
Licata, D. R., & Harper, R. (2011). 2-dimensional directed type theory. Electronic Notes in Theoretical Computer Science, 276, 263–289. https://doi.org/10.1016/j.entcs.2011.09.026. Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).
Licata, D. R., & Finster, E. (2014). Eilenberg-MacLane spaces in homotopy type theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS’14 (pp. 66:1–66:9). New York: ACM. https://doi.org/10.1145/2603088.2603153
Lurie, J. (2009). Higher topos theory, Annals of mathematics studies (Vol. 170). Princeton: Princeton University Press. https://doi.org/10.1515/9781400830558
Mandell, M., May, J., Schwede, S., & Shipley, B. (2001). Model categories of diagram spectra. Proceedings of the London Mathematical Society (3), 82(2), 441–512. https://doi.org/10.1112/S0024611501012692
Mautner, F. (1946). An extension of Klein’s Erlanger Program: Logic as invariant-theory. American Journal of Mathematics 68(3), 345–384. https://doi.org/10.2307/2371821
Mazel-Gee, A. (2016). Quillen adjunctions induce adjunctions of quasicategories. New York Journal of Mathematics, 22, 57–93. http://nyjm.albany.edu/j/2016/22-4.html
Nuyts, A. (2015). Towards a directed homotopy type theory based on 4 kinds of variance. Ph.D. thesis, KU Leuven. https://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf
Quillen, D. (1967). Homotopical algebra (Vol. 43). Cham: Springer. https://doi.org/10.1007/BFb0097438
Quine, W. V. O. (1969). Ontological relativity and other essays. New York/London: Columbia University Press.
Riehl, E., & Shulman, M. (2017). A type theory for synthetic ∞-categories. Higher Structures, 1(1), 147–224. https://journals.mq.edu.au/index.php/higher_structures/article/view/36
Rijke, E. (2017). The join construction. https://arxiv.org/abs/1701.07538. Preprint.
Rijke, E., Shulman, M., & Spitters, B. (2017). Modalities in homotopy type theory. https://arxiv.org/abs/1706.07526. Preprint.
Rodin, A. (2017). Venus homotopically. IfCoLog Journal of Logics and Their Applications, 4(4), 1427–1445. http://collegepublications.co.uk/ifcolog/?00013. Special Issue Dedicated to the Memory of Grigori Mints. Dov Gabbay and Oleg Prosorov (Guest Editors).
Schreiber, U. (2016). Modern Physics formalized in modal homotopy type theory. https://ncatlab.org/schreiber/show/Modern+Physics+formalized+in+Modal+Homotopy+Type+Theory, nLab
Schreiber, U., & Shulman, M. (2019). Model of type theory in an (∞, 1)-topos. https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos Revision 19, Homotopy Type Theory wiki.
Schreiber, U., & Shulman, M. (2018). n-types cover. https://ncatlab.org/nlab/show/n-types+cover. Revision 6, nLab.
Serre, J. P. (1953). Cohomologie modulo 2 des complexes d’Eilenberg-MacLane. Commentarii Mathematici Helvetici, 27, 198–232. https://doi.org/10.1007/BF02564562
Shulman, M. (2014). Homotopy type theory should eat itself (but so far, it’s too big to swallow). https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/. Blog post.
Shulman, M. (2017). Elementary (∞, 1)-topoi. https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html. Blog post.
Tarski, A. (1986). What are logical notions? History and Philosophy of Logic, 7(2), 143–154. https://doi.org/10.1080/01445348608837096. Ed. by J. Corcoran.
Tsementzis, D. (2017). Univalent foundations as structuralist foundations. Synthese, 194(9), 3583–3617. https://doi.org/10.1007/s11229-016-1109-x
Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study.
van Doorn, F. (2016). Constructing the propositional truncation using non-recursive hits. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (pp. 122–129). https://doi.org/10.1145/2854065.2854076
van Doorn, F. (2018). On the formalization of higher inductive types and synthetic homotopy theory. Ph.D. thesis, Carnegie Mellon University.
van Doorn, F., von Raumer, J., & Buchholtz, U. (2017). Homotopy type theory in Lean. In M. Ayala-Rincón & C. Muñoz (Eds.), ITP 2017: Interactive theorem proving, Lecture notes in computer science (Vol. 10499). Cham: Springer. https://doi.org/10.1007/978-3-319-66107-0_30
Voevodsky, V. (2013). A simple type system with two identity types. https://ncatlab.org/homotopytypetheory/files/HTS.pdf. Started 23 Feb 2013. Work in progress.
Voevodsky, V. (2014). The origins and motivations of univalent foundations. The IAS Institute Letter. https://www.ias.edu/ideas/2014/voevodsky-origins
Voevodsky, V. (2015). An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5), 1278–1294. https://doi.org/10.1017/S0960129514000577
Voevodsky, V., Ahrens, B., Grayson, D., et al. (2014). UniMath – a computer-checked library of univalent mathematics. Available at https://github.com/UniMath/UniMath
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Buchholtz, U. (2019). Higher Structures in Homotopy Type Theory. In: Centrone, S., Kant, D., Sarikaya, D. (eds) Reflections on the Foundations of Mathematics. Synthese Library, vol 407. Springer, Cham. https://doi.org/10.1007/978-3-030-15655-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-15655-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-15654-1
Online ISBN: 978-3-030-15655-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)