Globular weak $ω$-categories as models of a type theory
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917580499845120 |
|---|---|
| author | Benjamin, Thibaut Finster, Eric Mimram, Samuel |
| author_facet | Benjamin, Thibaut Finster, Eric Mimram, Samuel |
| contents | We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2106_04475 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Globular weak $ω$-categories as models of a type theory Benjamin, Thibaut Finster, Eric Mimram, Samuel Logic in Computer Science Category Theory We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak $ω$-groupoids: Those are defined as suitable presheaves over a cat-coherator, which is a category encoding structure expected to be found in an $ω$-category. This comparison is established by proving the initiality conjecture for the type theory CaTT, in a way which suggests the possible generalization to a nerve theorem for a certain class of dependent type theories |
| title | Globular weak $ω$-categories as models of a type theory |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2106.04475 |