Re: [HoTT] Non-enumerability of R

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

On Mon, Jul 17, 2017 at 03:52:28PM +0200, Andrej Bauer wrote:
> > In fact, no appeal to Stone-Weierstraß is needed, because that one is
> > about *uniform* approximation of functions, whereas we only need local
> > approximation. Yes?
> 
> It's still easier than that, isn't it already the case that the
> constant functions taking a rational value suffice? On every open
> interval every continuous map intersects one of those.

At  www.mathematik.tu-darmstadt.de/~streicher/rnc.pdf you find a
littele note of mine where I fill in some details in the
Rosolini-Spitters argument that Sh(R) doesn't validate the statement
that for every sequenc a in R^D there is a b in R^D with b # a_n for
all n (# stands for "apart").

But this argument doesn't show that

   \neg \exists a : N -> R. \forall b : R. \exists n:N. a_n = b

fails in Sh(R). I don't know any topos where this fails.

Thomas