The types in Martin-Löf type theory have, by virtue of the identity types, the structure of ∞-groupoids, as shown by van den Berg and Garner, and Lumsdaine. However, there are many higher-dimensional categorical structures which are not groupoidal. In this talk we will discuss such structures in the context of type theory. In particular, we will describe a type theory in which types form (∞, ∞)-categories.