Types are internal ∞-groupoids

Eric Finster, Matthieu Sozeau, Antoine Allioux

Research output: Chapter in Book/Report/Conference proceedingConference contribution

26 Downloads (Pure)


By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode a number of fully coherent algebraic structures. In particular, our approach leads to a definition of ∞-groupoid internal to type theory and we prove that the type of such ∞-groupoids is equivalent to the universe of types. That is, every type admits the structure of an ∞-groupoid internally, and this structure is unique.
Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages13
ISBN (Print)9781665448956, 9781665448963 (PoD)
Publication statusPublished - 7 Jul 2021

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871
ISSN (Electronic)2575-5528


Dive into the research topics of 'Types are internal ∞-groupoids'. Together they form a unique fingerprint.

Cite this