Syllepsis in Homotopy Type Theory

TL;DR

This paper demonstrates that the syllepsis property, known in classical topology, also holds in homotopy type theory for 3-loops, extending the Eckmann-Hilton theorem to higher dimensions.

Contribution

It proves that syllepsis, a higher-dimensional symmetry property, holds in homotopy type theory, extending classical topological results to the HoTT framework.

Findings

Syllepsis holds for 3-loops in HoTT.

Eckmann-Hilton proofs for p and q are inverses.

Extends classical topology results to higher homotopy levels.

Abstract

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.