Document Open Access Logo

The ∞-Category of ∞-Categories in Simplicial Type Theory

Authors Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.52.pdf
  • Filesize: 1.01 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
  • Theory of computation → Semantics and reasoning
Keywords
  • Type theory
  • Homotopy type theory
  • Category theory
  • Infinity category theory

Metrics

Abstract

Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about (∞,1)-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of ∞-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initially for cubical type theory to construct the ∞-category of spaces. We complete this process by constructing the ∞-category of ∞-categories, recovering one of the main foundational results of ∞-category theory (straightening-unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle: the structure homomorphism principle.

Cite As Get BibTex

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The ∞-Category of ∞-Categories in Simplicial Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 52:1-52:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.52

Author Details

Daniel Gratzer
  • Department of Computer Science, Aarhus University, Denmark
Jonathan Weinberger
  • Fowler School of Engineering, Chapman University, Orange, CA, USA
Ulrik Buchholtz
  • School of Computer Science, University of Nottingham, UK

Funding

  • Gratzer, Daniel: This work was supported in part by Villum Investigator grants (VIL73403 and VIL25804), Center for Basic Research in Program Verification (CPV), from Villum Fonden.
  • Weinberger, Jonathan: I thank the Fowler of School of Engineering at Chapman University for generous support of this work. I am particularly grateful to the Fletcher Jones Foundation and their award of a Fletcher Jones Foundation Faculty Fellowship in Engineering '25-'28 and the ensuing generous funding of this work. I also thank the Schmid School of Science and Technology as well as the Center of Excellence in Computation, Algebra, and Topology (CECAT), both at Chapman University, for my affiliation with them.

Acknowledgements

We thank the anonymous reviewers for their helpful feedback. We furthermore thank Rob Schellingerhout for observing that our initial definition of locally cocartesian families - now renamed "coherently locally cocartesian" - already implies cocartesianness.

References

  1. Benedikt Ahrens, Paige Randall North, and Niels van der Weide. Bicategorical type theory: semantics and syntax. Mathematical Structures in Computer Science, 33(10):868-912, October 2023. URL: https://doi.org/10.1017/s0960129523000312.
  2. César Bardomiano Martínez. Exponentiable functors between synthetic ∞-categories. Mathematical Structures in Computer Science, 35, 2025. URL: https://doi.org/10.1017/S0960129525100339.
  3. César Bardomiano Martínez. Limits and colimits in synthetic ∞-categories. Mathematical Structures in Computer Science, 35, 2025. URL: https://doi.org/10.1017/S0960129525100248.
  4. Ulrik Buchholtz and Jonathan Weinberger. Synthetic fibered (∞,1)-category theory. Higher Structures, 7:74-165, 2023. URL: https://doi.org/10.21136/HS.2023.04.
  5. Denis-Charles Cisinski, Bastiaan Cnossen, Kim Nguyen, and Tashi Walde. Synthetic category theory, 2025. Book in progress. URL: https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view.
  6. Denis-Charles Cisinski and Hoang Kim Nguyen. The universal cocartesian fibration, 2022. URL: https://arxiv.org/abs/2210.08945.
  7. Daniel Gratzer. Syntax and semantics of modal type theory. PhD thesis, Aarhus University, 2023. Google Scholar
  8. Daniel Gratzer, G.A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394736.
  9. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory, 2024. URL: https://doi.org/10.48550/arXiv.2407.09146.
  10. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The yoneda embedding in simplicial type theory. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 127-142. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00017.
  11. Fabian Hebestreit, Gijs Heuts, and Jaco Ruit. A short proof of the straightening theorem. Transactions of the American Mathematical Society, Series B, 12(19):697-747, May 2025. URL: https://doi.org/10.1090/btran/225.
  12. André Joyal. The theory of quasi-categories. Online, 2008. URL: https://math.uchicago.edu/~may/PEOPLE/JOYAL/0newqcategories.pdf.
  13. G.A. Kavvos. A quantum of direction. Online, 2019. URL: https://seis.bristol.ac.uk/~tz20861/papers/meio.pdf.
  14. F. William Lawvere. Axiomatic cohesion. Theory and Applications of Categories, 19(3):41-49, 2007. URL: http://www.tac.mta.ca/tac/volumes/19/3/19-03.pdf.
  15. Daniel R. Licata and Robert Harper. 2-dimensional directed type theory. Electronic Notes in Theoretical Computer Science, 276:263-289, September 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.026.
  16. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  17. Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009. Google Scholar
  18. Jacob Lurie. Higher algebra, 2017. Book draft. URL: https://www.math.ias.edu/~lurie/papers/HA.pdf.
  19. Louis Martini. Cocartesian fibrations and straightening internal to an ∞-topos, 2022. URL: https://arxiv.org/abs/2204.00295.
  20. Louis Martini and Sebastian Wolf. Presentability and topoi in internal higher category theory, 2025. URL: https://arxiv.org/abs/2209.05103.
  21. David Jaz Myers and Mitchell Riley. Commuting cohesions, 2023. URL: https://arxiv.org/abs/2301.13780.
  22. Jacob Neumann. A Generalized Algebraic Theory of Directed Equality. PhD thesis, University of Nottingham, 2025. Google Scholar
  23. Jacob Neumann. A judgmental construction of directed type theory, 2025. URL: https://doi.org/10.48550/arXiv.2510.17494.
  24. Jacob Neumann and Thorsten Altenkirch. The category interpretation of directed type theory. Online, 2024. URL: https://jacobneu.github.io/research/preprints/catModel-2024.pdf.
  25. Paige Randall North. Towards a directed homotopy type theory, 2018. URL: https://arxiv.org/abs/1807.10566.
  26. Andreas Nuyts. Towards a directed homotopy type theory based on 4 kinds of variance. Master’s thesis, KU Leuven, 2015. Google Scholar
  27. Andreas Nuyts. A vision for natural type theory, 2020. URL: https://anuyts.github.io/files/nattt-vision.pdf.
  28. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  29. Charles Rezk. A model for the homotopy theory of homotopy theory. Trans. Amer. Math. Soc., 353(3):973-1007, 2001. URL: https://doi.org/10.1090/S0002-9947-00-02653-2.
  30. Emily Riehl. Could ∞-category theory be taught to undergraduates? Notices of the American Mathematical Society, 70(5), 2023. URL: https://doi.org/10.1090/noti2692.
  31. Emily Riehl. Synthetic perspectives on spaces and categories, 2025. URL: https://arxiv.org/abs/2510.15795.
  32. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1:147-224, 2017. URL: https://doi.org/10.21136/HS.2017.06.
  33. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  34. Mitchell Riley. A type theory with a tiny object, 2024. URL: https://doi.org/10.48550/arXiv.2403.01939.
  35. Rob Schellingerhout. Higher algebra in simplicial homotopy type theory. Master’s thesis, Utrecht University, 2026. Forthcoming. Google Scholar
  36. Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856-941, 2018. URL: https://doi.org/10.1017/S0960129517000147.
  37. Michael Shulman. All (∞,1)-toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004.
  38. Jan M. Smith. Propositional functions and families of types. Notre Dame Journal of Formal Logic, 30(3), June 1989. URL: https://doi.org/10.1305/ndjfl/1093635159.
  39. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. URL: https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  40. Michael Warren. Directed type theory. Online, April 2013. Seminar talk. URL: https://www.ias.edu/video/univalent/1213/0410-MichaelWarren.
  41. Matthew Z. Weaver and Daniel R. Licata. A constructive model of directed univalence in bicubical sets. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20. ACM, July 2020. URL: https://doi.org/10.1145/3373718.3394794.
  42. Matthew Zachary Weaver. Bicubical Directed Type Theory. PhD thesis, Princeton University, 2024. URL: http://arks.princeton.edu/ark:/88435/dsp017s75dg778.
  43. Jonathan Weinberger. A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects. PhD thesis, Technische Universität Darmstadt, 2022. URL: https://doi.org/10.26083/tuprints-00020716.
  44. Jonathan Weinberger. Internal sums for synthetic fibered (∞,1)-categories. Journal of Pure and Applied Algebra, 228(9):107659, September 2024. URL: https://doi.org/10.1016/j.jpaa.2024.107659.
  45. Jonathan Weinberger. Two-sided cartesian fibrations of synthetic (∞,1)-categories. Journal of Homotopy and Related Structures, 19(2), June 2024. URL: https://doi.org/10.1007/s40062-024-00348-3.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact