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