On the Hierarchy of Univalent Universes: Un is not n-Truncated

In recent years, it has become clear that types in intensional Martin-Löf Type Theory can be seen as spaces, alternatively to the traditional view as sets or propositions. This observation motivated Voevodsky’s univalence axiom and the development of a whole branch of mathematics, known as Univalent Foundations and Homotopy Type Theory (HoTT). One of the most basic consequences of univalence is that the type-theoretic universe U0 does not have unique identity proofs. We show a generalization of this result: universe Un is not n-truncated, meaning that it has a non-trivial homotopical structure above dimension n. Our solu-tion also answers the related (and so far open) problem of the Univalent Foundations Program in Princeton (2012/2013) of constructing a type that strictly has some high truncation level without using higher induc-tive types. Further, we present a construction for the dual notion, connectedness. Given a type, we construct (in plain Martin-Löf Type Theory without HoTT-axioms) a type that is equivalent to the original one above a given dimension n. We show that it is trivial on all lower dimensions in the sense of a predicate we define, and that this predicate is equivalent to saying that the type is n-connected if the theory supports truncations. We have fully formalized and verified our results within the depen-dently typed language and proof assistant Agda.