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”.

We also have a pdf version of the proof.

About Nicolai Kraus

At the University of Nottingham
This entry was posted in Code, Foundations, Talk, Univalence. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s