1: \begin{abstract}

2: %

3: \textcite{riehl:2017} introduced \emph{simplicial type theory} (\STT), a variant of homotopy type

4: theory which aimed to study not just homotopy theory, but its fusion with category theory:

5: $\prn{\infty,1}$-category theory. While notoriously technical, manipulating $\infty$-categories in

6: simplicial type theory is often easier than working with ordinary categories, with the type theory

7: handling infinite stacks of coherences in the background. We capitalize on recent work by

8: \textcite{gratzer:2024} defining the $\prn{\infty,1}$-category of $\infty$-groupoids in \STT{} to define presheaf categories

9: within \STT{} and systematically develop their theory. In particular, we construct the Yoneda

10: embedding, prove the universal property of presheaf categories, refine the theory of adjunctions

11: in \STT{}, introduce the theory of Kan extensions, and prove Quillen's Theorem A. In addition to

12: a large amount of category theory in \STT{}, we offer substantial evidence that \STT{} can be

13: used to produce difficult results in $\infty$-category theory at a fraction of the complexity.

14: 

15: %

16: %

17: %

18: %

19:  \end{abstract}

20: