Non-enumerability of R

[Andrew Swan <wakeli...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 926 bytes --]

I don't have an answer, but I've also wondered about this question, so I'll add some more remarks of my own.

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.

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.

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.

Best,
Andrew