[FOM] Challenge addressed by HoTT/UF that is not addressed by ZFC

[Ben Sherman]

Dimitris Tsementzis <dtsement at princeton.edu> on April 4, 2016, writes:

> Concerning (2): In HoTT/UF, this issue is addressed almost as a triviality. The type Set in a univalent universe U can be given the structure of a category and it contains *all* sets in U (defined as types of h-level 0, i.e. discrete homotopy types). The reason this works so well is because in HoTT/UF a given universe U is not comprised of sets. Sets are merely one of many structures one can impose on the objects of U. It thus becomes as natural to speak of *all* sets as it is in ZFC to speak of *all* sets of a given rank.

> (b) Furthermore, it is an especially compelling example since it cannot be repeated in traditional (non-HoTT) MLTT. It depends essentially on having a notion of the h-level of a type and formalizing sets as types of a specific h-level.

I don't believe this is the case. See section 3.5 (Subsets and propositional resizing) of the HoTT book. The notion of h-level is not related to universe-levels. In general, for a fixed h-level, there are types with that h-level which can be expressed in a given universe level but not a lower universe level. So for instance, one cannot quantify over all h-sets at once (though this is often hidden in the notation since universe levels are left implicit). The one exception is for the the lowest h-level, -1, which correspond to propositions, where one may admit an axiom called propositional resizing, which makes the universe of propositions impredicative, so that one may quantify over all propositions (as is done in Coq).

The ranks in the von Neumann hierarchy are still analogous to the universe levels in either Martin-Löf type theory of HoTT.