Higher Eckmann-Hilton Arguments in Type Theory
Higher Eckmann-Hilton Arguments in Type Theory
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 …