arXiv Open Access 2021

Types are Internal $\infty$-Groupoids

Antoine Allioux Eric Finster Matthieu Sozeau

Lihat Sumber

Abstrak

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 $\infty$-groupoid internal to type theory and we prove that the type of such $\infty$-groupoids is equivalent to the universe of types. That is, every type admits the structure of an $\infty$-groupoid internally, and this structure is unique.

Topik & Kata Kunci

cs.LO math.CT

Penulis (3)

Antoine Allioux

Eric Finster

Matthieu Sozeau

Format Sitasi

APA MLA BibTeX

Allioux, A., Finster, E., Sozeau, M. (2021). Types are Internal $\infty$-Groupoids. https://arxiv.org/abs/2105.00024

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2021
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓