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

[Freek Wiedijk]

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