DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.52

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

Authors: Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{gratzer_et_al:LIPIcs.LICS.2026.52,
  author =	{Gratzer, Daniel and Weinberger, Jonathan and Buchholtz, Ulrik},
  title =	{{The ∞-Category of ∞-Categories in Simplicial Type Theory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{52:1--52:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.52},
  URN =		{urn:nbn:de:0030-drops-268393},
  doi =		{10.4230/LIPIcs.LICS.2026.52},
  annote =	{Keywords: Type theory, Homotopy type theory, Category theory, Infinity category theory}
}

Search Results

Documents authored by Weinberger, Jonathan

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

Abstract

Cite as

Thanks for your feedback!

Could not send message