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

[Dimitris Tsementzis]

> On Apr 5, 2016, at 06:15, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> Of course you can have a category SET of "all" sets in standard
> f.o.m., as long as you do not demand that SET is a set.

Well, yes, but this is just like having “large” and “small” sets and SET being the category of all “small” sets, similar to all other proposed solutions. It is a kind of solution, but not an ideal one. And in my opinion not as good as the one in HoTT/UF.

> In particular, I just do not believe that this "issue" of a universal
> object comes anywhere near close to any
> kind of reason to overhaul the usual standard f.o.m. that has been so
> firmly in place since around 1920.
> 
> I'll change my mind on a dime if I see something comparatively simple, and there
> is something specific and compelling that you gain that is far more
> specific than what
> Dmitiris is suggesting. Just the general idea that there is a
> universal object is simply much too amorphous to be a reason. What do
> you want to do with a universal object that is so terrific?

I’m not sure exactly what you mean by a “universal object” though I can see that in some sense SET is one. Is it fair to ask for an explanation? 

Also, of course, the ISSUE I raised was not meant to be a definitive reason to switch foundations, but an illustration of the kind of thing that “alternative f.o.m.” allows you to do well, that you can also do in standard f.o.m. but not so well. 

Dimitris