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, recovering one of the main foundational results of $\infty$-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.

翻译：单纯类型论（STT）由 Riehl 与 Shulman 引入，旨在利用同伦类型理论来证明关于 $(\infty,1)$-范畴的结果。早期对单纯类型论的研究主要集中于高阶范畴论中的“形式”论证，特别是，在 STT 中无法构造出非平凡的∞-范畴论实例。近期的工作改变了这一状况，通过应用最初为立方类型论开发的技术，构造了空间的∞-范畴。我们通过构造∞-范畴的∞-范畴来完成这一进程，从而纯粹在类型论的意义上恢复了∞-范畴理论的一个主要基础性结果（拉直–反拉直）。我们还展示了这一构造如何为结构同态原理的定向版本提供新的实例。