Syllepsis in Homotopy Type Theory

Kristina Sojakova; G.A. Kavvos

doi:10.1145/3531130.3533347

Syllepsis in Homotopy Type Theory

Kristina Sojakova
, G.A. Kavvos

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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 sufciently 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.

Original language	English
Title of host publication	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9781450393515
DOIs	https://doi.org/10.1145/3531130.3533347
Publication status	Published - 2 Aug 2022
Externally published	Yes
Event	37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Conference

Conference	37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Country/Territory	Israel
City	Haifa
Period	2/08/22 → 5/08/22

Funding

The first author gratefully acknowledges the support of the ANR TECAP grant (decision number ANR-17-CE39-0004-03).

Access to Document

10.1145/3531130.3533347

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{3f0e5c396cb44539815954a06c2ed01a,

title = "Syllepsis in Homotopy Type Theory",

abstract = "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 sufciently 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{\"o}f type theory.",

author = "Kristina Sojakova and G.A. Kavvos",

year = "2022",

month = aug,

day = "2",

doi = "10.1145/3531130.3533347",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

booktitle = "Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022",

address = "United States",

note = "37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 ; Conference date: 02-08-2022 Through 05-08-2022",

}

Sojakova, K & Kavvos, GA 2022, Syllepsis in Homotopy Type Theory. in Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022., 3533347, Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, Haifa, Israel, 2/08/22. https://doi.org/10.1145/3531130.3533347

Syllepsis in Homotopy Type Theory. / Sojakova, Kristina; Kavvos, G.A.
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. Institute of Electrical and Electronics Engineers Inc., 2022. 3533347 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Syllepsis in Homotopy Type Theory

AU - Sojakova, Kristina

AU - Kavvos, G.A.

PY - 2022/8/2

Y1 - 2022/8/2

N2 - 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 sufciently 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.

AB - 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 sufciently 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.

UR - https://www.scopus.com/pages/publications/85132054761

UR - https://www.scopus.com/pages/publications/85132054761#tab=citedBy

U2 - 10.1145/3531130.3533347

DO - 10.1145/3531130.3533347

M3 - Conference contribution

T3 - Proceedings - Symposium on Logic in Computer Science

BT - Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022

Y2 - 2 August 2022 through 5 August 2022

ER -

Syllepsis in Homotopy Type Theory

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this