A type theory for invertibility in weak $ω$-categories
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914337551024128 |
|---|---|
| author | Benjamin, Thibaut Champin, Camil Markakis, Ioannis |
| author_facet | Benjamin, Thibaut Champin, Camil Markakis, Ioannis |
| contents | We present a conservative extension ICaTT of the dependent type theory CaTT for weak $ω$-categories with a type witnessing coinductive invertibility of cells. This extension allows for a concise description of the "walking equivalence" as a context, and of a set of maps characterising $ω$-equifibrations as substitutions. We provide an implementation of our theory, which we use to formalise basic properties of invertible cells. These properties allow us to give semantics of ICaTT in marked weak $ω$-categories, building a fibrant marked $ω$-category out of every model of ICaTT. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_16602 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A type theory for invertibility in weak $ω$-categories Benjamin, Thibaut Champin, Camil Markakis, Ioannis Category Theory Logic in Computer Science We present a conservative extension ICaTT of the dependent type theory CaTT for weak $ω$-categories with a type witnessing coinductive invertibility of cells. This extension allows for a concise description of the "walking equivalence" as a context, and of a set of maps characterising $ω$-equifibrations as substitutions. We provide an implementation of our theory, which we use to formalise basic properties of invertible cells. These properties allow us to give semantics of ICaTT in marked weak $ω$-categories, building a fibrant marked $ω$-category out of every model of ICaTT. |
| title | A type theory for invertibility in weak $ω$-categories |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2602.16602 |