Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories?
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913985408794624 |
|---|---|
| author | Rasekh, Nima |
| author_facet | Rasekh, Nima |
| contents | $\infty$-category theory was originally developed in the context of classical homotopy theory using standard set theoretical assumptions, but has since been extended to a variety of mathematical foundations. One such successful effort, primarily due to Martini and Wolf, introduced a theory of $\infty$-categories internal to the foundation of an arbitrary Grothendieck $\infty$-topos, meaning they used categorical foundations. Another approach, due to Riehl and Shulman, developed a theory of $\infty$-categories internal to their own type theory: simplicial homotopy type theory (sHoTT), meaning they employed a (homotopy) type theoretic foundation.
One aspect of developing a theory of $\infty$-categories in different foundations consists of introducing ways to translate from one foundation to another. Concretely, as part of their work, Riehl and Shulman prove that $\infty$-categories internal to Grothendieck $\infty$-topoi give us categorical models of sHoTT. In fact the name ``simplicial'' in sHoTT suggests that all categorical models of sHoTT should be given by simplicial objects in suitable $\infty$-categories. In this paper we prove that contrary to this expectation, there are models of sHoTT that are not simply simplicial objects. This suggests that in a general foundations, the notion of $\infty$-category is more general than previously assumed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_07737 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories? Rasekh, Nima Category Theory Logic 18N60, 03B38, 03G30, 18N40, 18C50, 03H05 $\infty$-category theory was originally developed in the context of classical homotopy theory using standard set theoretical assumptions, but has since been extended to a variety of mathematical foundations. One such successful effort, primarily due to Martini and Wolf, introduced a theory of $\infty$-categories internal to the foundation of an arbitrary Grothendieck $\infty$-topos, meaning they used categorical foundations. Another approach, due to Riehl and Shulman, developed a theory of $\infty$-categories internal to their own type theory: simplicial homotopy type theory (sHoTT), meaning they employed a (homotopy) type theoretic foundation. One aspect of developing a theory of $\infty$-categories in different foundations consists of introducing ways to translate from one foundation to another. Concretely, as part of their work, Riehl and Shulman prove that $\infty$-categories internal to Grothendieck $\infty$-topoi give us categorical models of sHoTT. In fact the name ``simplicial'' in sHoTT suggests that all categorical models of sHoTT should be given by simplicial objects in suitable $\infty$-categories. In this paper we prove that contrary to this expectation, there are models of sHoTT that are not simply simplicial objects. This suggests that in a general foundations, the notion of $\infty$-category is more general than previously assumed. |
| title | Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories? |
| topic | Category Theory Logic 18N60, 03B38, 03G30, 18N40, 18C50, 03H05 |
| url | https://arxiv.org/abs/2508.07737 |