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

[Dimitris Tsementzis]

Dear Freek,

> I think HoTT is built upon a type theory with a hierarchy of
> type universes?  I always think of Type_0 as "small" types,
> and Type_1 as "large" types. 

Yes, the difference I was trying to point out is between sets in HoTT and general types. The same kind of issues arise for small and large types in HoTT. But there is a way to look at it so that they don’t arise for sets in HoTT, if one takes very seriously the idea that sets in HoTT are not primitive. (My replies to Ben Sherman and Francois Dorais tried to clarify this.)

Dimitris

> On Apr 11, 2016, at 05:05, Freek Wiedijk <freek at cs.ru.nl> wrote:
> 
> Dear Dimitris,
> 
>> All of the methods above involve "large" and "small"
>> sets in one form or another.
> 
> I think HoTT is built upon a type theory with a hierarchy of
> type universes?  I always think of Type_0 as "small" types,
> and Type_1 as "large" types.  So it seems exactly the same
> thing to me, only with a countable number of iterations.
> Which is not _that_ much of a difference.
> 
> (In Tarski-Grothendieck set theory one iterates not just
> a countable number of times like this, but has a universe
> like Type_i for each ordinal number.)
> 
> Freek
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom