Bibliographic Details
| Title: |
Higher Eckmann-Hilton Arguments in Type Theory |
| Authors: |
Benjamin, Thibaut, Markakis, Ioannis, Offord, Wilfred, Sarti, Chiara, Vicary, Jamie |
| Publication Year: |
2025 |
| Collection: |
Computer Science
Mathematics |
| Subject Terms: |
Mathematics - Category Theory, Computer Science - Logic in Computer Science |
| More Details: |
We use a type theory for omega-categories to produce higher-dimensional generalisations of the Eckmann-Hilton argument. The heart of our construction is a family of padding and repadding techniques, which give a notion of congruence between cells of different types. This gives explicit witnesses in all dimensions that, for cells with degenerate boundary, all composition operations are congruent and commutative. Our work has been implemented, allowing us to explicitly compute these witnesses, and we show these grow rapidly in complexity as the parameters are varied. Our results can also be exported as elements of identity types in Martin-Lof type theory, and hence are of relevance in homotopy type theory. |
| Document Type: |
Working Paper |
| Access URL: |
http://arxiv.org/abs/2501.16465 |
| Accession Number: |
edsarx.2501.16465 |
| Database: |
arXiv |
