Re: [HoTT] Non-enumerability of R

[Gaetan Gilbert <gaetan....@ens-lyon.fr>]

I don't see how to do R -> 3^N/~ where R is HIT reals (without choice, 
ofc with choice we can just go through quotiented cauchy sequences).

Gaëtan Gilbert

On 18/07/2017 16:41, Nicolai Kraus wrote:
> 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 <mailto: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
>     <mailto:HomotopyTypeTheo...@googlegroups.com>.
>     For more options, visit https://groups.google.com/d/optout
>     <https://groups.google.com/d/optout>.
>
>
> -- 
> 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 
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.