一句话：在单纯类型论中构造预层范畴与 Yoneda 嵌入，并发展 ∞-范畴论工具。
单纯类型论（STT）是 homotopy type theory 的变体，旨在研究同伦论与范畴论融合而成的 (∞,1)-范畴论，但在其中操作 ∞-范畴仍技术复杂。本文基于 Gratzer 等人在 STT 中定义 ∞-groupoid 的 (∞,1)-范畴的工作，在 STT 内部定义预层范畴并系统发展其理论。作者构造 Yoneda 嵌入，证明预层范畴的万有性质，细化 STT 中的伴随理论，引入 Kan 扩张理论，并证明 Quillen 定理 A。这些结果不仅给出大量 STT 内的范畴论内容，也提供有力证据：STT 能以远低于传统方法的复杂度产出 ∞-范畴论中的困难结果。
Riehl and Shulman [1] introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: (∞, 1)-category theory. While notoriously technical, manipulating ∞-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. [2] defining the (∞, 1)-category of ∞-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen’s Theorem A. In addition to a large amount of category theory in STT, we offer substantial evidence that STT can be used to produce difficult results in ∞-category theory at a fraction of the complexity.