Elementary $\infty$-toposes from type theory
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911740369829888 |
|---|---|
| author | Apol, Daniël Petrowitsch, Maximilian |
| author_facet | Apol, Daniël Petrowitsch, Maximilian |
| contents | We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\infty$-localisation an elementary $\infty$-topos, that is, a finitely complete, locally cartesian closed $\infty$-category with enough univalent universal morphisms. We also show that elementary $\infty$-toposes have small subobject classifiers. To achieve this, we extend Joyal's theory of tribes by introducing the notion of a univalent tribe and a univalent fibration in a tribe. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_18891 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Elementary $\infty$-toposes from type theory Apol, Daniël Petrowitsch, Maximilian Category Theory Algebraic Topology Logic We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\infty$-localisation an elementary $\infty$-topos, that is, a finitely complete, locally cartesian closed $\infty$-category with enough univalent universal morphisms. We also show that elementary $\infty$-toposes have small subobject classifiers. To achieve this, we extend Joyal's theory of tribes by introducing the notion of a univalent tribe and a univalent fibration in a tribe. |
| title | Elementary $\infty$-toposes from type theory |
| topic | Category Theory Algebraic Topology Logic |
| url | https://arxiv.org/abs/2512.18891 |