U_n is not an n-Type

[Nicolai Kraus]

I have uploaded a note to the wiki with a proof of the following:

In MLTT with a hierarchy of univalent universes, the n-th universe is
not an n-type.

This is a generalization of the fact that U_0 is not a set. Univalence
is the only HoTT-axiom that is used (no truncations, not HITs). At the
same time, the note provides a solution for one of the questions in the
"open problems" section of the wiki: I construct a type that is an
(n+1)-type, but not an n-type.
I have started to formalize the proof in Agda, but I won't have time to
finish it in the next days; but I will definitely do it soon (just not
very soon).
The note is quite short - if people are interested, I can give a
presentation about the proof, explaining what is going on.

Nicolai

[Nicolai Kraus]

Sorry, I forgot to provide a link:

uf-ias-2012.wikispaces.com/file/view/hierarchy.pdf/420248220/hierarchy.pdf

[Andrej Bauer]

Should this go in the book?

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Nicolai Kraus]

Andrej, good question. I will present the proof, I think, on Monday.
Let's discuss it after that.
Nicolai

[Nicolai Kraus]

Just to let you know, I have formalized the proof that "Universe n is
not an n-type" (on which I gave a talk in Princeton earlier this month).

Here is an html-version of the Agda code:
http://red.cs.nott.ac.uk/~ngk/hierarchy/Hierarchy.html

It uses the "old" HoTT-github Agda library though, which will soon be
replaced (right?), I can adapt it when that happens. Also, my Agda code
is not very readable. Christian Sattler and I are going to write a post
for the HoTT-blog, which (I hope) will serve as a better informal
explanation.

Best wishes to everyone!
Nicolai