The Yoneda embedding in simplicial type theory
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917137666277376 |
|---|---|
| author | Gratzer, Daniel Weinberger, Jonathan Buchholtz, Ulrik |
| author_facet | Gratzer, Daniel Weinberger, Jonathan Buchholtz, Ulrik |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_13229 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Yoneda embedding in simplicial type theory Gratzer, Daniel Weinberger, Jonathan Buchholtz, Ulrik Logic in Computer Science Algebraic Topology Category Theory 03B38, 18N60, 18D30, 18B50, 18N45, 55U35, 18N50 F.4.1 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. |
| title | The Yoneda embedding in simplicial type theory |
| topic | Logic in Computer Science Algebraic Topology Category Theory 03B38, 18N60, 18D30, 18B50, 18N45, 55U35, 18N50 F.4.1 |
| url | https://arxiv.org/abs/2501.13229 |