  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.
