Types are Internal $\infty$-Groupoids

Antoine Allioux, Eric Finster, Matthieu Sozeau

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…