Re: [HoTT] Non-enumerability of R

[Nicolai Kraus <nicola...@gmail.com>]

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

Hi Andrej and everyone reading the discussion,

I don't know the answer, but here's a related construction/question.
Let's say we use "book HoTT" to have a precise definition for "surjective"
and so on, but let's not fix a concrete incarnation of constructive reals
R.
As you said, 2^N is not an accepted definition of the reals (it shouldn't
be,
since we would expect that a functions R -> 2 which we can write down is
constant).

Let's write 3 := {0,1,2} and consider the quotient Q := (3^N)/~, where ~
relates
two sequences f,g : N -> 3 if both f and g have a "2" in their image.  (In
other
words, we keep 2^N untouched and squash the whole rest into a single
equivalence class; this can directly be expressed as a HIT without any
truncations, by giving a point 'seq(f)' for every sequence f : N -> 3, a
point 'other',
and an equality 'seq(f) = other' for every f that contains a 2.)

Question: For which definition of the real numbers R does the projection
3^N ->> 3^N/~ factor through R as in
  (*)  3^N >-> R ->> 3^N/~
        (injection followed by a surjection)?

  (**) Can we show that there is no surjection N -> 3^N/~,
        or what is the status of this?

The point is that most definitions of constructive reals are somewhat
involved,
while 3^N/~ seems a bit simpler.  (*) and (**) together imply that there is
no
surjection N ->> R.

For example, if R is the Cauchy reals that are defined to be "Cauchy
sequences
N -> Q that are quotiented afterwards", then we can construct (*), e.g. by
mapping f to the Cauchy sequence s(f)_n := sum_{i = 0..n} 1/4^i * fi, where
the '4'
guarantees that s is injective.  Vice versa, given a Cauchy sequence c, we
can
construct a sequence r(c) : N -> 3 as follows.  To find r(c)_{n+1}, we
check whether
the limit of c "has a chance" to lie in the interval between
s(c0, c1, ..., cn, 0, 0, 0, ...) and s(c0, c1, ..., cn, 0, 1, 1, 1, ...)
where "having a chance" means that the difference between the interval
boundaries
and c_N is small enough (where "N" and "small enough" depend only on n and
the
 rate of convergency in the definition of Cauchy reals).  If there "is a
chance", we
choose r(c)_{n+1} := 0.
Similarly, we can check whether there "is a chance" that r(c)_{n+1} must be
1.
We can define "there is a chance" such that there cannot be a chance for
both 0
and 1.  If there is no chance for either, we just choose r(c)_{n+1} := 2
and thus spoil
the whole sequence (it will necessarily lie in the "other" equivalence
class).

The above is very similar to an idea in our partiality paper [1].  For that
case,
Gaëtan Gilbert has refined the strategy so that it works with the higher
inductive-
inductive reals of the HoTT book.  Does (*) work for the HIIT reals as well?

Best regards,
Nicolai

[1] Altenkirch, Danielsson, K; Partiality, Revisited.
https://arxiv.org/abs/1610.09254
[2] Gilbert; Formalising Real Numbers in Homotopy Type Theory.
     https://arxiv.org/abs/1610.05072


On Wed, Jul 12, 2017 at 10:04 AM, Andrej Bauer <andrej...@andrej.com>
wrote:

> I have been haunted by the question "Is there a surjection from N to
> R?" in a constructive setting without choice. Do we know whether the
> following is a theorem of Unimath or some version of HoTT:
>
>      "There is no surjection from the natural numbers to the real numbers."
>
> Some remarks:
>
> 1. Any reasonable definition of real numbers would be acceptable, as
> long as you're not cheating with setoids. Also, since this is not set
> theory, the powerset of N and 2^N are not "reals".
>
> 2. It is interesting to consider different possible definitions of
> "surjection", some of which will probably turn out to have an easy
> answer.
>
> 3. In the presence of countable choice there is no surjection, by the
> usual proof. (But we might have to rethink the argument and place
> propositional truncations in the correct spots.)
>
> 4. It is known that there can be an injection from R into N, in the
> presence of depedent choice (in the realizability topos on the
> infinite-time Turing machines).
>
> With kind regards,
>
> Andrej
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 5600 bytes --]