Types are Internal \infty-Groupoids
From MaRDI portal
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 -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.
This page was built for publication: Types are Internal $\infty$-Groupoids
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6366549)
