|
2 | 2 |
|
3 | 3 | main: |
4 | 4 |
|
| 5 | + - title: Higher Eckmann-Hilton Arguments in Type Theory |
| 6 | + authors: Thibaut Benjamin, Ioannis Markakis, Wilfred Offord, Chiara Sarti, Jamie Vicary |
| 7 | + journal: Preprint |
| 8 | + date: 2025 |
| 9 | + pdf: https://arxiv.org/pdf/2501.16465.pdf |
| 10 | + arxiv : https://arxiv.org/abs/2501.16465 |
| 11 | + abstract: 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. |
| 12 | + doi: https://doi.org/10.48550/arXiv.2501.16465 |
| 13 | + |
| 14 | + - title: Naturality for higher-dimensional path types |
| 15 | + authors: Thibaut Benjamin, Ioannis Markakis, Wilfred Offord, Chiara Sarti, Jamie Vicary |
| 16 | + journal: Preprint |
| 17 | + date: 2025 |
| 18 | + pdf: https://arxiv.org/pdf/2501.11620.pdf |
| 19 | + arxiv : https://arxiv.org/abs/2501.11620 |
| 20 | + abstract: We define a naturality construction for the operations of weak \(\omega\)-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a ``power tool'' to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in omega-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants. |
| 21 | + doi: https://doi.org/10.48550/arXiv.2501.11620 |
| 22 | + |
5 | 23 | - title: Invertible cells in \(\omega\)-categories |
6 | 24 | authors: Thibaut Benjamin, Ioannis Markakis |
7 | 25 | journal: Preprint |
8 | 26 | date: 2024 |
9 | 27 | pdf: https://arxiv.org/pdf/2406.12127.pdf |
10 | 28 | arxiv : https://arxiv.org/abs/2406.12127 |
11 | | - abstract: We study coinductive invertibility of cells in weak \(\omega\)\-categories. We use the inductive presentation of weak \(\omega\)\-categories via an adjunction with the category of computads, and show that invertible cells are closed under all operations of $\omega$\-categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data. |
| 29 | + abstract: We study coinductive invertibility of cells in weak \(\omega\)\-categories. We use the inductive presentation of weak \(\omega\)\-categories via an adjunction with the category of computads, and show that invertible cells are closed under all operations of $\omega$\-categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data. |
12 | 30 | doi: https://doi.org/10.48550/arXiv.2406.12127 |
13 | 31 |
|
14 | 32 | - title: CaTT contexts are finite computads |
|
20 | 38 | abstract: Two novel descriptions of weak \(\omega\)-categories have been recently proposed, using type-theoretic ideas. The first one is the dependent type theory CaTT whose models are \(\omega\)-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 \(\omega\)-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. |
21 | 39 | doi: https://doi.org/10.48550/arXiv.2405.00398 |
22 | 40 |
|
23 | | - |
24 | 41 | - title: Opposites for weak \(\omega\)-categories and the suspension and hom adjunction |
25 | 42 | authors: Thibaut Benjamin, Ioannis Markakis |
26 | 43 | journal: Preprint |
|
0 commit comments