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

[François Dorais]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160410/a6254efd/attachment-0001.html>