CaTT contexts are finite computads
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916527504097280 |
|---|---|
| author | Benjamin, Thibaut Markakis, Ioannis Sarti, Chiara |
| author_facet | Benjamin, Thibaut Markakis, Ioannis Sarti, Chiara |
| contents | Two novel descriptions of weak ω-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are ω-categories. The second is a recursive description of a category of computads together with an adjunction to globular sets, such that the algebras for the induced monad are again ω-categories. We compare the two descriptions by showing that there exits a fully faithful morphism of categories with families from the syntactic category of CaTT to the opposite of the category of computads, which gives an equivalence on the subcategory of finite computads. We derive a more direct connection between the category of models of CaTT and the category of algebras for the monad on globular sets, induced by the adjunction with computads. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_00398 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | CaTT contexts are finite computads Benjamin, Thibaut Markakis, Ioannis Sarti, Chiara Category Theory Logic in Computer Science 18N65, 18N10, 18N30 F.4.1; I.2.3 Two novel descriptions of weak ω-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are ω-categories. The second is a recursive description of a category of computads together with an adjunction to globular sets, such that the algebras for the induced monad are again ω-categories. We compare the two descriptions by showing that there exits a fully faithful morphism of categories with families from the syntactic category of CaTT to the opposite of the category of computads, which gives an equivalence on the subcategory of finite computads. We derive a more direct connection between the category of models of CaTT and the category of algebras for the monad on globular sets, induced by the adjunction with computads. |
| title | CaTT contexts are finite computads |
| topic | Category Theory Logic in Computer Science 18N65, 18N10, 18N30 F.4.1; I.2.3 |
| url | https://arxiv.org/abs/2405.00398 |