Types are Internal $\infty$-Groupoids

TL;DR

This paper develops a type-theoretic framework to define and analyze internal $ abla$-groupoids, demonstrating that every type can be equipped with a unique internal $ abla$-groupoid structure, unifying algebraic and type-theoretic perspectives.

Contribution

It introduces a novel type-theoretic approach to internal $ abla$-groupoids using polynomial monads, establishing their equivalence to the universe of types.

Findings

Every type admits a unique internal $ abla$-groupoid structure.

The type of internal $ abla$-groupoids is equivalent to the universe of types.

The framework encodes fully coherent algebraic structures within type theory.

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.