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

[Dimitris Tsementzis]

Dear Ben, 

> On Apr 10, 2016, at 15:50, Ben Sherman <sherman at csail.mit.edu> wrote:
> 
> 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).

Of course you need a universe U to even define h-levels in U. h-sets are therefore always relative to a universe. But this is unrelated to the main point, which is a very simple one. Basic objects in UF are not sets, but homotopy types. Sets are defined as homotopy types of h-level 0. In a given universe U this gives me SET(U). From where I’m standing now (say a larger universe U’ containing U) I have a (type of) *all* h-sets in U. If I were to talk about h-sets in U’ I would have to also regard U’ as a universe and in that case, yes, SET(U) does not contain *all* h-sets. But I may simply not do this, and work with one universe. Now there are no h-levels in U’ and therefore there are no sets as far as I’m concerned. What remains are homotopy types and that’s that. From my perspective in U’ I have collected *all* h-sets in SET(U). Furthermore, U is not really to be understood as a “large” h-set similar to a “class” of all sets.

Now, yes, the book version of HoTT has countable nested universes. Therefore it is always possible to speak of sets in a larger universe. One gets the feeling, in doing so, that one is “missing out” on h-sets of a higher universe level. I am saying that I think this is the wrong way to look at it philosophically because h-sets are not “already” there. The only thing that is “already” there are homotopy types. And from a technical standpoint, not all HoTTs have to have countable universes. One can work with only one universe. In the case of one universe, it becomes clearer in what sense you can talk about *all* sets. 

There are of course many formal difficulties and intricacies involved: resizing, impredicativity, polymorphism etc. But these take away from the main point, which I want to repeat, because I think it is a very simple and deep down non-technical one (and the demand was for *simple* issues): In HoTT one can collect all sets together (in a suitable sense) in such a way that one is neither (1) collecting *all* one's basic objects together, nor (2) defining a “larger” set. (I am not saying the technical subtleties are irrelevant, of course, nor that they should not constrain what one says. But the demand was for an easily understandable challenge with an easily understandable solution: and I think the intuition behind both the challenge and the solution can be presented very simply and not inaccurately without mentioning these subtleties.)

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

Of course. “Size” issues apply just the same to *all* types. But sets types in HoTT are not sets.

Dimitris