Wiki. Eckmann–Hilton 论证 [Eckmann--Hilton论证]

Eckmann–Hilton 论证大致说的是, (在 $1$-范畴中) 两个相容的结合代数结构 (即 $\mathbb E_2$-代数) 会导致一个交换代数结构. 例如在 $\mathsf{Set}$ 中, 群对象中的群对象是 Abel 群: $$ \mathsf{Grp}(\mathsf{Grp}(\mathsf{Set})) \simeq \mathsf{Ab}. $$

陈述

同伦类型论

在同伦类型论中, Eckmann–Hilton 论证给出一个类型 $A$ 的元素 $a$ 的二阶环路空间 $\Omega^2 (A,a)$ 上两个元素复合的交换; 也即自反等价 $\mathsf{refl}_a$ 的两个自等价 $$ \alpha,\beta\colon \mathsf{refl}_a = \mathsf{refl}_a $$ 满足的等式 $$ \alpha\cdot\beta = \beta\cdot\alpha. $$