{"id":"arxiv/2602.02218","url":"https://arxiv.org/abs/2602.02218","tags":["cs.LO","math.CT"],"score":0,"title":"The $\\infty$-category of $\\infty$-categories in simplicial type theory","domain":"cs.LO","source":"arxiv","authors":["Daniel Gratzer","Jonathan Weinberger","Ulrik Buchholtz"],"reviews":0,"subject":"cs.LO","summary":"Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about $(\\infty,1)$-categories. Initial work on simplicial type theory focused on \"formal\" arguments in higher category theory and, in particular, no non-trivial examples of $\\infty$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the $\\infty$-category of spaces. We complete this process by constructing the $\\infty$-category of $\\infty$-categories,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-02","reactions":{}}