Beyond Eckmann-Hilton: Commutativity in Higher Categories

TL;DR

The paper tackles explicit commutativity of composition in weak $ω$-categories by providing a constructive, type-theoretic framework (CaTT) that generalizes the Eckmann-Hilton phenomenon to higher dimensions. It introduces padding and repadding techniques to produce parameterised equivalences $H^n_{k,l}(a,b)$ and derived Eckmann-Hilton witnesses $EH^n_{k,l}$, proving commutativity up to congruence for $n$-cells with degenerate boundaries and extending via dual paddings to an Eckmann-Hilton sphere. The approach is implemented in CaTT, with results exportable to identity types in Homotopy Type Theory, bridging syntactic type-theory machinery and synthetic homotopy theory. The work provides a robust, scalable method to compute higher-dimensional witnesses and supports the homotopy-theoretic program for ω-categories by delivering explicit algebraic witnesses and a formal verification framework.

Abstract

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.

Figures (16)

• Figure 1: Composites of a pair of $2$/̄cells.
• Figure 2: The equivalence $\mathop{\mathrm{H}}\nolimits : a *_1 b \to u_x^{-1} *_1 (a *_0 b) *_1 u_x$.
• Figure 3: The $3$-dimensional Eckmann-Hilton sphere.
• Figure 4: Construction of the base cases $\mathop{\mathrm{H}}\nolimits^n_{n-1,0}$ for the case $n=2$.
• Figure 5: The untyped syntax of $\mathsf{CaTT}$.

Theorems & Definitions (78)

• Definition 2.1
• Definition 2.2
• Definition 2.3: Sphere and Disc contexts
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Definition 2.7
• Definition 2.8
• Lemma 2.9
• Definition 2.10