The Yoneda embedding in simplicial type theory

TL;DR

This paper develops the theory of presheaf categories within simplicial type theory, including the Yoneda embedding, adjunctions, Kan extensions, and Quillen's Theorem A, facilitating easier manipulation of $( abla,1)$-categories.

Contribution

It systematically constructs presheaf categories and their fundamental properties in simplicial type theory, advancing the formalization of higher category theory within this framework.

Findings

Constructed the Yoneda embedding in STT

Proved the universal property of presheaf categories

Established Quillen's Theorem A in STT

Abstract

Riehl and Shulman 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: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-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. defining the $(\infty,1)$-category of $\infty$-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.