一句话：在 Martin-Löf 类型论中，利用 intensional identity type 的消去规则构造出 syllepsis 一致性单元。
Eckmann–Hilton 论证表明，同一集合上满足交换律的两个幺半群结构实际上是同一个可交换运算；当这些幺半群对应于足够高维范畴中的竖直与水平复合时，Eckmann–Hilton 论证本身表现为一个高维胞元。该胞元通常还需满足额外的一致性条件，即 syllepsis。本文研究该一致性条件在同伦类型论中的可构造性，证明可以在 Martin-Löf 类型论中从 intensional identity type 的消去规则出发构造出 syllepsis。工作以类型论推导给出形式化证明，为高阶范畴结构在类型论中的编码提供了一致性依据。
The Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids correspond to the vertical and horizontal composition of a sufficiently higher-dimensional category, the Eckmann-Hilton argument itself appears as a higher cell. This cell is often required to satisfy an additional piece of coherence, which is known as the syllepsis. We show that the syllepsis can be constructed from the elimination rule of intensional identity types in Martin-Löf type theory.