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