Beyond Eckmann-Hilton: Commutativity in Higher Categories

TL;DR

This paper generalizes the Eckmann-Hilton argument to higher-dimensional weak globular omega-categories, showing that certain composition operations are equivalent and commutative, with constructive type-theoretic methods and computational implementations.

Contribution

It introduces a higher-dimensional generalization of Eckmann-Hilton, with padding techniques and a constructive type-theoretic framework for omega-categories.

Findings

All composition operations are equivalent and commutative under certain conditions.

Constructive methods allow explicit computation of witnesses.

Implementation enables extraction of witnesses as inhabitants of identity types.

Abstract

We show that in a weak globular $\omega$-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 $\omega$-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.