From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.148.23 with SMTP id w23mr249665wmd.0.1500388867146; Tue, 18 Jul 2017 07:41:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.88.11 with SMTP id m11ls255179ljb.11.gmail; Tue, 18 Jul 2017 07:41:05 -0700 (PDT) X-Received: by 10.25.211.8 with SMTP id k8mr344435lfg.2.1500388865245; Tue, 18 Jul 2017 07:41:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500388865; cv=none; d=google.com; s=arc-20160816; b=lJtMkm+r5z+5k44GvmLHt2gAoLUydBpwbTygoDJwlQcSF2TAoRbBxyRDzkdB8piX+G BxwVV0Gzbgwmp49p+ajRPD+SadJ23ITRZd53qYEktlWYB8dT7Z7+coEA6Fl7pnul24O0 RlmUgLAR/sAXpAPF39PeU6ER3dcVtx6QV1BUcuQzjopOxIPzhCxMONdOpSbZhaue+Taq VeztrWBYHyLtDESyC/rEDEJrHQAG2FwMKzLWKQ3GiR9KcKK5l/pulc4iiui4GtbFjAKQ ogiGrG9h4tsEMWwpnvvhceP3XLYoDe7o5KxGOoEfoHk54ZXXDqvVLVSH//mFXUxj6GF1 /KUg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=hrJV/xxlnwW4b50DLUQpvTMe/CVoL131OJRg3d3pqo4=; b=h6WSHHAtX/LdbkTLT/MfLhFESvNfr2YxMZsjKiF5ihWug854GJFva7Wj+MhDMbZr86 VFtpzJrxUFFGnMdUSSgQyOnB1Aad/Avw8cK9XGAN7meDA2dH56v310g2pwD5xG+Rc9+3 1RggYIISObpDywfFYzn0Lm5euaAFyC62RN0ohKiTDuC6UotmzSsm0HUYnXotOKSGuOaj GPIwCeKUGT6/R63T+ojrgZfz/wRjDhDf0eafMCEuNRYXD94zH2rxormjr61CkZcCDPM/ tZPsbAM9DQgB5xPoJXj63GHgxrNIK90qVrMX+5/qZFsOxIVyFO3Vap3RzSqUC5TbkAXH tjYw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=DOsoijzP; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-lf0-x22b.google.com (mail-lf0-x22b.google.com. [2a00:1450:4010:c07::22b]) by gmr-mx.google.com with ESMTPS id z4si4686656wmb.0.2017.07.18.07.41.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 18 Jul 2017 07:41:05 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) client-ip=2a00:1450:4010:c07::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=DOsoijzP; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4010:c07::22b as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22b.google.com with SMTP id t72so15867755lff.1 for ; Tue, 18 Jul 2017 07:41:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=hrJV/xxlnwW4b50DLUQpvTMe/CVoL131OJRg3d3pqo4=; b=DOsoijzPqMZj1latZUmnb3S/qs7LdFfMc98tTYhD/nl9vpQeXnqrrswG5jE/4WS0AQ ip1rFJjujIZVi+d2P+StkpnvlSpd5iC+jcHI/7xAlBAr0+RcPa3hmzR+eVt1mlHFcYlo InBf+7j/Rnn5NDxnFXgYDLAgSY03rd8UE8eV4pjGrWSjIGYBFVG15+NBbONkVkvEPWbd 9lNgpOanglTEFh1pyqhP2sD2BhMrMLctWIL9QRx77PHoAolFN8qinBdb7zeseXOyvHyA B0M6ku1XGQpf6+KEF2tl/7/sEqwYKIpVpYlEAGIGjIMHzJ3RNO4Tz8Pgir85lCZfEseg BaUw== X-Gm-Message-State: AIVw110jySNmBN6XWRqWZx+nWYiODDQuZj3ejIMGGuvxvI3n/HrUmIyG k3sYEj9PKJbt84orVpeAxjQZzjguYC8Z X-Received: by 10.46.9.82 with SMTP id 79mr809984ljj.89.1500388864825; Tue, 18 Jul 2017 07:41:04 -0700 (PDT) MIME-Version: 1.0 Received: by 10.46.84.88 with HTTP; Tue, 18 Jul 2017 07:41:03 -0700 (PDT) In-Reply-To: References: From: Nicolai Kraus Date: Tue, 18 Jul 2017 15:41:03 +0100 Message-ID: Subject: Re: [HoTT] Non-enumerability of R To: Andrej Bauer Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="001a114b0af0501eb30554988164" --001a114b0af0501eb30554988164 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 :=3D {0,1,2} and consider the quotient Q :=3D (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) =3D 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 :=3D sum_{i =3D 0..n} 1/4^i * fi, w= here 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} :=3D 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} :=3D 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=C3=ABtan Gilbert has refined the strategy so that it works with the high= er 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 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. > --001a114b0af0501eb30554988164 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Andrej and everyone reading the discussion,

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

Let's write 3 :=3D {0,1,2} and consider the quotient Q :=3D = (3^N)/~, where ~ relates
two sequences f,g : N -> 3 if both f and g = have a "2" in their image.=C2=A0 (In other
words, we keep 2^N= untouched and squash the whole rest into a single
equivalence class; t= his can directly be expressed as a HIT without any
truncations, by givi= ng a point 'seq(f)' for every sequence f : N -> 3, a point '= other',
and an equality 'seq(f) =3D 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
=C2= =A0 (*)=C2=A0 3^N >-> R ->> 3^N/~
=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 (injection followed by a surjection)?

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

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

For example, if R is the C= auchy reals that are defined to be "Cauchy sequences
N -> Q tha= t are quotiented afterwards", then we can construct (*), e.g. by
m= apping f to the Cauchy sequence s(f)_n :=3D sum_{i =3D 0..n} 1/4^i * fi, wh= ere the '4'
guarantees that s is injective.=C2=A0 Vice versa, gi= ven a Cauchy sequence c, we can
construct a sequence r(c) : N -> 3 a= s follows.=C2=A0 To find r(c)_{n+1}, we check whether
the limit of c &q= uot;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 "havi= ng a chance" means that the difference between the interval boundaries=
and c_N is small enough (where "N" and "small enough&qu= ot; depend only on n and the
=C2=A0rate of convergency in the definition= of Cauchy reals).=C2=A0 If there "is a chance", we
choose r(= c)_{n+1} :=3D 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&= quot; such that there cannot be a chance for both 0
and 1.=C2=A0 If the= re is no chance for either, we just choose r(c)_{n+1} :=3D 2 and thus spoil=
the whole sequence (it will necessarily lie in the "other" eq= uivalence class).

The above is very similar to an idea in our parti= ality paper [1].=C2=A0 For that case,
Ga=C3=ABtan Gilbert has refined t= he strategy so that it works with the higher inductive-
inductive reals = of the HoTT book.=C2=A0 Does (*) work for the HIIT reals as well?

Be= st regards,
Nicolai

[1] Altenkirch, Danielsson, K; Partiality, Re= visited. https://arxiv.org/abs= /1610.09254
[2] Gilbert; Formalising Real Numbers in Homotopy Type T= heory.
=C2=A0=C2=A0=C2=A0=C2=A0 https://arxiv.org/abs/1610.05072


On Wed, Jul 12, 2017 at 10:04 AM, Andrej B= auer <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:

=C2=A0 =C2=A0 =C2=A0"There is no surjection from the natural numbers t= o 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 eas= y
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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114b0af0501eb30554988164--