Re: [HoTT] Non-enumerability of R

[Andrej Bauer <andrej...@andrej.com>]

Dear Andrew,

thank you for your remarks.

> 1. In the topos of sheaves over the closed unit interval the Dedekind reals are not uncountable (in fact there is a countably enumerable "double negation dense set" in the reals). I think it's reasonable to expect the same thing in Thierry Coquand's cubical stack model and so show the same is consistent with HoTT.

For the uninitiated, let me just clarify that one such not-not-dense
countable subset is the set P of polynomials with rational
coefficients. One then appeals to density of this set by the
Stone-Weierstraß theorem: for every continuous function on every open
set there is some polynomial in P which intersects its graph, hence R
\ P is empty.

Let us call a set/object/type X *inexhaustible* when for every
sequence a : N → X there is some x in X which is different from all
terms of the sequence. An inexhaustible set clearly is not countable.
What your remark shows is that the reals cannot be shown to be
inexhaustible in intuitionistic logic without choice.


> 2. I would conjecture that constructing cubical sets internally in the infinite time Turing machine topos gives a model of HoTT with an injection from the reals to the naturals.

Yes, but note by your third remarks, that as soon as there is an
injection from reals to natural numbers, there can be no surjection
going the other way. So cubical sets in infinite-time HoTT won't
resolve the question.

> 3. There is an entirely constructive proof that there is no bijection between the naturals and the reals (for any reasonable definition of real): first if there is an injection then the reals have decidable equality, but then this yields a proof that there is no surjection by a standard diagonal argument.

Neat.

With kind regards,

Andrej