The $\infty$-category of $\infty$-categories in simplicial type theory

Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz

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 th…