Higher Structures in Homotopy Type Theory

  • Ulrik BuchholtzEmail author
Part of the Synthese Library book series (SYLI, volume 407)


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.


  1. Ahrens, B., Kapulkin, K., & Shulman, M. (2015). Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25(5), 1010–1039. CrossRefGoogle Scholar
  2. 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. Google Scholar
  3. 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.Google Scholar
  4. 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. CrossRefGoogle Scholar
  5. 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.
  6. Angiuli, C., & Harper, R. (2018). Meaning explanations at higher dimension. Indagationes Mathematicae, 29(1), 135–149. L.E.J. Brouwer, fifty years later.CrossRefGoogle Scholar
  7. Annenkov, D., Capriotti, P., & Kraus, N. (2017). Two-level type theory and applications. Preprint.
  8. Awodey, S. (2014). Structuralism, invariance, and univalence. Philosophia Mathematica (3), 22(1), 1–11. CrossRefGoogle Scholar
  9. Awodey, S. (2018). Univalence as a principle of logic. Indagationes Mathematicae. CrossRefGoogle Scholar
  10. Baez, J. (2007). The homotopy hypothesis. Lecture at Higher Categories and Their Applications, Thematic Program on Geometric Applications of Homotopy Theory, Fields Institute, Toronto.
  11. 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. Google Scholar
  12. Boardman, J., & Vogt, R. (1973). Homotopy invariant algebraic structures on topological spaces (Vol. 347). Cham: Springer.CrossRefGoogle Scholar
  13. Brunerie, G. (2016). On the homotopy groups of spheres in homotopy type theory. Ph.D. thesis, Laboratoire J.A. Dieudonné.
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. Buchholtz, U., & Favonia (Hou), K. B. (2018). Cellular cohomology in homotopy type theory. Accepted for Proceedings of Logic in Computer Science (LICS 2018).
  17. Buchholtz, U., & Rijke, E. (2018). The Cayley-Dickson construction in homotopy type theory. To appear in Higher Structures.Google Scholar
  18. Buchholtz, U., van Doorn, F., & Rijke, E. (2018). Higher groups in homotopy type theory. Accepted for Proceedings of Logic in Computer Science (LICS 2018).
  19. Capriotti, P., & Kraus, N. (2017). Univalent higher categories via complete semi-Segal types. Preprint.
  20. 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. Google Scholar
  21. 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. Google Scholar
  22. 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.CrossRefGoogle Scholar
  23. Grothendieck, A. (1983). Pursuing stacks. Manuscript.
  24. Harpaz, Y. (2015). Quasi-unital -categories. Algebraic & Geometric Topology, 15(4), 2303–2381. CrossRefGoogle Scholar
  25. Joyal, A. (2002). Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175(1–3), 207–222. CrossRefGoogle Scholar
  26. Kan, D. M. (1956). Abstract homotopy. III. Proceedings of the National Academy of Sciences of the United States of America, 42, 419–421. CrossRefGoogle Scholar
  27. Klein, F. (1872). Vergleichende Betrachtungen über neuere geometrische Forschungen. Verlag von Andreas Deichert, Erlangen.Google Scholar
  28. 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. CrossRefGoogle Scholar
  29. Kraus, N., & Sattler, C. (2015). Higher homotopies in a hierarchy of univalent universes. ACM Transactions on Computational Logic, 16(2), 18:1–18:12. CrossRefGoogle Scholar
  30. Licata, D. R., & Harper, R. (2011). 2-dimensional directed type theory. Electronic Notes in Theoretical Computer Science, 276, 263–289. Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).CrossRefGoogle Scholar
  31. 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.
  32. Lurie, J. (2009). Higher topos theory, Annals of mathematics studies (Vol. 170). Princeton: Princeton University Press. Google Scholar
  33. 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. CrossRefGoogle Scholar
  34. Mautner, F. (1946). An extension of Klein’s Erlanger Program: Logic as invariant-theory. American Journal of Mathematics 68(3), 345–384. CrossRefGoogle Scholar
  35. Mazel-Gee, A. (2016). Quillen adjunctions induce adjunctions of quasicategories. New York Journal of Mathematics, 22, 57–93. Google Scholar
  36. Nuyts, A. (2015). Towards a directed homotopy type theory based on 4 kinds of variance. Ph.D. thesis, KU Leuven.
  37. Quillen, D. (1967). Homotopical algebra (Vol. 43). Cham: Springer. CrossRefGoogle Scholar
  38. Quine, W. V. O. (1969). Ontological relativity and other essays. New York/London: Columbia University Press.CrossRefGoogle Scholar
  39. Riehl, E., & Shulman, M. (2017). A type theory for synthetic -categories. Higher Structures, 1(1), 147–224. Google Scholar
  40. Rijke, E. (2017). The join construction. Preprint.
  41. Rijke, E., Shulman, M., & Spitters, B. (2017). Modalities in homotopy type theory. Preprint.
  42. Rodin, A. (2017). Venus homotopically. IfCoLog Journal of Logics and Their Applications, 4(4), 1427–1445. Special Issue Dedicated to the Memory of Grigori Mints. Dov Gabbay and Oleg Prosorov (Guest Editors).
  43. Schreiber, U. (2016). Modern Physics formalized in modal homotopy type theory., nLab
  44. Schreiber, U., & Shulman, M. (2019). Model of type theory in an (, 1)-topos.,1)-topos Revision 19, Homotopy Type Theory wiki.
  45. Schreiber, U., & Shulman, M. (2018). n-types cover. Revision 6, nLab.
  46. Serre, J. P. (1953). Cohomologie modulo 2 des complexes d’Eilenberg-MacLane. Commentarii Mathematici Helvetici, 27, 198–232. CrossRefGoogle Scholar
  47. Shulman, M. (2014). Homotopy type theory should eat itself (but so far, it’s too big to swallow). Blog post.
  48. Shulman, M. (2017). Elementary (, 1)-topoi. Blog post.
  49. Tarski, A. (1986). What are logical notions? History and Philosophy of Logic, 7(2), 143–154. Ed. by J. Corcoran.CrossRefGoogle Scholar
  50. Tsementzis, D. (2017). Univalent foundations as structuralist foundations. Synthese, 194(9), 3583–3617. CrossRefGoogle Scholar
  51. Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics., Institute for Advanced Study.
  52. 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).
  53. van Doorn, F. (2018). On the formalization of higher inductive types and synthetic homotopy theory. Ph.D. thesis, Carnegie Mellon University.Google Scholar
  54. 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. Google Scholar
  55. Voevodsky, V. (2013). A simple type system with two identity types. Started 23 Feb 2013. Work in progress.
  56. Voevodsky, V. (2014). The origins and motivations of univalent foundations. The IAS Institute Letter. Google Scholar
  57. Voevodsky, V. (2015). An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5), 1278–1294. CrossRefGoogle Scholar
  58. Voevodsky, V., Ahrens, B., Grayson, D., et al. (2014). UniMath – a computer-checked library of univalent mathematics. Available at Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Fachbereich MathematikTU DarmstadtDarmstadtGermany

Personalised recommendations