We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Types are Internal $\infty$-Groupoids

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 $\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.
Comments: Extended version of the LICS 2021 article
Subjects: Logic in Computer Science (cs.LO); Category Theory (math.CT)
Cite as: arXiv:2105.00024 [cs.LO]
  (or arXiv:2105.00024v1 [cs.LO] for this version)

Submission history

From: Matthieu Sozeau [view email]
[v1] Fri, 30 Apr 2021 18:10:15 GMT (42kb,D)

Link back to: arXiv, form interface, contact.