Beyond Eckmann-Hilton: Commutativity in Higher Categories
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917155393503232 |
|---|---|
| author | Benjamin, Thibaut Markakis, Ioannis Offord, Wilfred Sarti, Chiara Vicary, Jamie |
| author_facet | Benjamin, Thibaut Markakis, Ioannis Offord, Wilfred Sarti, Chiara Vicary, Jamie |
| contents | We show that in a weak globular $ω$-category, all composition operations are equivalent and commutative for cells with sufficiently degenerate boundary, which can be considered a higher-dimensional generalisation of the Eckmann-Hilton argument. Our results are formulated constructively in a type-theoretic presentation of $ω$-categories. The heart of our construction is a family of padding and repadding techniques, which gives an equivalence relation between cells which are not necessarily parallel. Our work has been implemented, allowing us to explicitly compute suitable witnesses, which grow rapidly in complexity as the dimension increases. These witnesses can be exported as inhabitants of identity types in Homotopy Type Theory, and hence are of relevance in synthetic homotopy theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_16465 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Beyond Eckmann-Hilton: Commutativity in Higher Categories Benjamin, Thibaut Markakis, Ioannis Offord, Wilfred Sarti, Chiara Vicary, Jamie Category Theory Logic in Computer Science 18N65, 18N30, 03B38, 68V20 We show that in a weak globular $ω$-category, all composition operations are equivalent and commutative for cells with sufficiently degenerate boundary, which can be considered a higher-dimensional generalisation of the Eckmann-Hilton argument. Our results are formulated constructively in a type-theoretic presentation of $ω$-categories. The heart of our construction is a family of padding and repadding techniques, which gives an equivalence relation between cells which are not necessarily parallel. Our work has been implemented, allowing us to explicitly compute suitable witnesses, which grow rapidly in complexity as the dimension increases. These witnesses can be exported as inhabitants of identity types in Homotopy Type Theory, and hence are of relevance in synthetic homotopy theory. |
| title | Beyond Eckmann-Hilton: Commutativity in Higher Categories |
| topic | Category Theory Logic in Computer Science 18N65, 18N30, 03B38, 68V20 |
| url | https://arxiv.org/abs/2501.16465 |