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

[Dimitris Tsementzis]

Dear Francois,

> Could you explain how HoTT can talk about *all* sets? I've been trying to understand what you mean and here is what I arrived at.

My reply to Ben Sherman contains my explanation. 

> I understand I can form the type SET_i of all sets in a universe level U_i. The resulting type SET_i is a type in the next universe level U_{i+1}. However, U_{i+1} has more sets than U_i and so SET_i does not have *all* sets from the point of view of U_{i+1}. Admittedly, since SET_i is not itself a set, it is not immediately obvious that U_{i+1} must have more sets than U_i. One can see that U_{i+1} does indeed have more sets than U_i by recasting the Burali-Forti paradox in HoTT (see Section 10.3 of the HoTT Book for the necessary ingredients).

Yes, but suppose I am “inside” U_{i+1}. Then Set_{i+1} does not exist for me. To define it, I need to view U_{i+1} also as a universe. (As I said to Ben Sherman, in book HoTT one can always do this because we are assuming countable universes; but it’s not necessary to do this.) Therefore, from inside U_{i+1} the only sets I can see are the terms of Set_{i}. Everything else is a homotopy type. There are no “large” sets for me since I cannot define h-levels in the universe I’m sitting in. Here it becomes very clear in what sense sets are a derived notion in HoTT, not a primitive one.

(I agree with everything you say regarding Burali-Forti and large and small sets when comparing two universes. I am merely explaining a different point of view in which you are within a universe and do not allow yourself to regard it as a universe.)

> 3. Universe polymorphism does seem like a good way to take a global look at all SET_i together, but this device doesn't seem much different than the use of set-theoretic universes by Mac Lane, Grothendieck and others.

I think I disagree. In usual type theory, yes, perhaps I share your view. But in HoTT, with a well-understood distinction between types and sets, and where universes are made up of homotopy types, I think the situation is relevantly different that the Mac Lane, Grothendieck etc. approaches. I grant that this is maybe a matter of taste though. And in any case I don’t think it affects the above points.

Dimitris


> On Apr 10, 2016, at 03:01, François Dorais <francois at dorais.org> wrote:
> 
> Dear Dimitris:
> 
> I never doubted that there are such work-arounds. My contention is that they are not as satisfactory as what you can do in HoTT (with respect to this issue). All of the methods above involve “large” and “small” sets in one form or another. So there will be sets that you are leaving out when defining SET. In HoTT this doesn’t happen. This is to be expected, because in HoTT not all its basic objects are sets. The basic objects are homotopy types. This allows you to easily talk about all sets, since not all homotopy types are sets.
> 
> There is absolutely nothing complicated going on here other than the natural evolution of ideas. Set theory gave a foundation to mathematics. Mathematics also advanced because of set theory. Sets thus became objects of study of actual day-to-day mathematics, rather than just ways to formalize mathematics. So now we need natural foundations which can talk of *all* sets as if they were just one more among many (non-primitive) mathematical structures. HoTT provides one such way.
> 
> Could you explain how HoTT can talk about *all* sets? I've been trying to understand what you mean and here is what I arrived at.
> 
> I understand I can form the type SET_i of all sets in a universe level U_i. The resulting type SET_i is a type in the next universe level U_{i+1}. However, U_{i+1} has more sets than U_i and so SET_i does not have *all* sets from the point of view of U_{i+1}. Admittedly, since SET_i is not itself a set, it is not immediately obvious that U_{i+1} must have more sets than U_i. One can see that U_{i+1} does indeed have more sets than U_i by recasting the Burali-Forti paradox in HoTT (see Section 10.3 of the HoTT Book for the necessary ingredients).
> 
> After some pondering, it seems that if I assume propositional resizing (more precisely, that PROP_i is equivalent to PROP_{i+1}) then the sets from U_{i+1} that are missing from SET_i are precisely the ones that are too large. Indeed, suppose X is a set in U_{i+1} and Y is a set in U_i. If f:X -> Y is an embedding in U_{i+1}, then the range of f must actually exist as a subset of Y in U_i by propositional resizing. In U_{i+1}, X is equivalent to the range of f and therefore X is equivalent to an element of SET_i. It follows that the sets from U_{i+1} that are missing from SET_i are precisely the "large" sets that can't be embedded into "small" sets from U_i.
> 
> It seems to me that the situation in HoTT is not that different from that in ZFC/NBG:
> 
> 1. SET_i is a type consisting of *all* sets in the universe U_i but SET_i is not a type in U_i.
> 
> 2. SET_i is a type in U_{i+1} but it only consists of the sets which are "small" (and "simple", if we don't assume propositional resizing).
> 
> 3. Universe polymorphism does seem like a good way to take a global look at all SET_i together, but this device doesn't seem much different than the use of set-theoretic universes by Mac Lane, Grothendieck and others.
> 
> Perhaps I missed something, but I can't think of any other ways to understand what you mean by "talk of *all* sets as if they were just one more among many (non-primitive) mathematical structures" in HoTT.
> 
> Best,
> François G. Dorais
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160411/3ab89635/attachment-0001.html>