Types are internal infinity-groupoids - Archive ouverte HAL Access content directly
Conference Papers Year :

Types are internal infinity-groupoids

(1, 2) , (3, 4) , (3, 5)
1
2
3
4
5

Abstract

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.
Fichier principal
Vignette du fichier
types-are-grpds-ext.pdf (320.58 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03133144 , version 1 (05-02-2021)
hal-03133144 , version 2 (05-01-2022)

Identifiers

  • HAL Id : hal-03133144 , version 2

Cite

Eric Finster, Antoine Allioux, Matthieu Sozeau. Types are internal infinity-groupoids. LICS 2021, Jun 2021, Rome, Italy. ⟨hal-03133144v2⟩
309 View
688 Download

Share

Gmail Facebook Twitter LinkedIn More