@inproceedings{gratzer-2026-the,
  doi = {10.4230/LIPICS.LICS.2026.52},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.52},
  author = {Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
  keywords = {Type theory, Homotopy type theory, Category theory, Infinity category theory, Theory of computation, Theory of computation → Type theory, Theory of computation → Constructive mathematics, Theory of computation → Semantics and reasoning},
  language = {en},
  title = {The ∞-Category of ∞-Categories in Simplicial Type Theory},
  volume = {380},
  pages = {52:1-52:26},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2026},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)}
}