It is well-known that in homotopy type theory (HoTT), one can prove the Eckmann-Hilton theorem: given two 2-loops p, q : 1 = 1 on the reflexivity path at an arbitrary point a : A, we have pq = qp. If we go one dimension higher, i.e., if p and q are 3-loops, we show that a property classically known as syllepsis also holds in HoTT: namely, the Eckmann-Hilton proof for q and p is the inverse of the Eckmann-Hilton proof for p and q.

翻译：众所周知,在同质类型理论(Hott)中,人们可以证明埃克曼-希尔顿理论:在任意点a的反反射路径上,给两个2-卢普p, q: 1=1:A,我们有pq=qp。如果我们走高一个维度,即,如果p和q是3-卢普,我们显示,典型的、称为Syllepsis的属性在霍特也有:即,Eckmann-希尔顿对q和p的证据是埃克曼-希尔顿对p和q的证据的反面。