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

[François Dorais]

Dear Dimitris,

On Mon, Apr 11, 2016 at 6:34 PM, Dimitris Tsementzis <dtsement at princeton.edu
> wrote:

>
> Of course you need a universe U to even define h-levels in U. h-sets are
> therefore always relative to a universe. But this is unrelated to the main
> point, which is a very simple one. Basic objects in UF are not sets, but
> homotopy types. Sets are defined as homotopy types of h-level 0. In a given
> universe U this gives me SET(U). From where I’m standing now (say a larger
> universe U’ containing U) I have a (type of) *all* h-sets in U. If I were
> to talk about h-sets in U’ I would have to also regard U’ as a universe and
> in that case, yes, SET(U) does not contain *all* h-sets. But I may simply
> not do this, and work with one universe. Now there are no h-levels in U’
> and therefore there are no sets as far as I’m concerned. What remains are
> homotopy types and that’s that. From my perspective in U’ I have collected
> *all* h-sets in SET(U). Furthermore, U is not really to be understood as a
> “large” h-set similar to a “class” of all sets.



> Now, yes, the book version of HoTT has countable nested universes.
> Therefore it is always possible to speak of sets in a larger universe. One
> gets the feeling, in doing so, that one is “missing out” on h-sets of a
> higher universe level. I am saying that I think this is the wrong way to
> look at it philosophically because h-sets are not “already” there. The only
> thing that is “already” there are homotopy types. And from a technical
> standpoint, not all HoTTs have to have countable universes. One can work
> with only one universe. In the case of one universe, it becomes clearer in
> what sense you can talk about *all* sets.
>


I'm afraid I'm even more puzzled now. I don't see the need for a universe
in order to recognize that a type X is a set, I only need to check that the
type a = b is a proposition for all a, b : X, i.e. that any p, q: a = b are
equal. (I do need a universe U to form SET(U) but that goes without
saying.) The point is that if I have a universe U, then I can form the type
Ord(U) of all ordinals in U and I can recognize that Ord(U) is a set
(Theorems 10.3.10 and 10.3.20 from the HoTT Book). I can also see that
Ord(U) is not equivalent to any set in SET(U). This should work in your
version of HoTT since I never appealed to the existence of a higher
universe. In other words, if I can form the type SET(U) then I can also
form a set which is not equivalent to any type in SET(U). This seems to
contradict your claims (1) and (2) below, though I'm not sure exactly what
you mean in (2).



> There are of course many formal difficulties and intricacies involved:
> resizing, impredicativity, polymorphism etc. But these take away from the
> main point, which I want to repeat, because I think it is a very simple and
> deep down non-technical one (and the demand was for *simple* issues): In
> HoTT one can collect all sets together (in a suitable sense) in such a way
> that one is neither (1) collecting *all* one's basic objects together, nor
> (2) defining a “larger” set. (I am not saying the technical subtleties are
> irrelevant, of course, nor that they should not constrain what one says.
> But the demand was for an easily understandable challenge with an easily
> understandable solution: and I think the intuition behind both the
> challenge and the solution can be presented very simply and not
> inaccurately without mentioning these subtleties.)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160413/ca7e9879/attachment.html>