Universe n is not an n-Type

Joint work with Christian Sattler

Some time ago, at the UF Program in Princeton, I presented a proof that Universe n is not an n-type. We have now formalized that proof in Agda and want to present it here.

One of the most basic consequences of the univalence axiom is that the universe of types is not a set, i.e. does not have unique identity proofs. It is plausible to expect that the next universe $U_1$ is not a groupoid, i.e. its path-spaces are not sets, but a proof of that is already surprinsingly difficult.

We prove the generalized statement, namely that $U_n$ is not an n-type. At the same time, our construction yields, for a given $n$ , a type that is an $(n+1)$ -type but not an n-type. This answers one of the questions asked at the UF Program. The proof works in basic MLTT with $\Sigma$ -, $\Pi$ – and identity types as well as a sequence of universes. We need the uivalence axiom, but no other “HoTT-features”.