From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.20.67 with SMTP id 3mr393981lju.31.1500391719873; Tue, 18 Jul 2017 08:28:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.125.139 with SMTP id y133ls27931lfc.27.gmail; Tue, 18 Jul 2017 08:28:38 -0700 (PDT) X-Received: by 10.25.156.81 with SMTP id f78mr378169lfe.29.1500391718209; Tue, 18 Jul 2017 08:28:38 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500391718; cv=none; d=google.com; s=arc-20160816; b=OUuHSfulDNAgEmhx8Cr0/a+coSiR/qr5wVNl/Sx4wHLgblgpYc+B7E3lwdeY7aAOnz 4R7ir8MH2YNVGUg8DBIOipPWVdVJXTaC0waCTC6WRb3Ja4Q+I10djp+a9xuw7rtzu7cC 5Fx68tCJMAv2VMR58bTTSpBVaDZkk2nXd2w0aBQnUbonzVc0Hb2WfxZcyDXK+/XwNA4s 6nCHy9kLh7OJroJtUQnxFydPfSigMuLYcYwyRdhDOv4IVP6SFn8I3L3hufLNRcQHGGWN 62Wg5W38iMs7k57VG/WAcFAaIiH72lRgB1dA0l40dNcUnsGs56qwGFBlFpAv8wBrVEFw XzKA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :arc-authentication-results; bh=r0o+7ovVaJgB/aNyLfCVj1qqm8hABzF5XUxqAxsccYo=; b=m3IBMzH3cDWmN2sTzxPr9cxwis+tsBJGMCnAzAYv7B/2quItkYDGLsHmCtSRLZ8aiS u9wsoqV8OYptNz0k3ayIppxqm0wllKpi0REmm6jkNcfTCiEBTIcRLsK0fEAvNWzGUvyk cWuwWLu/R4riWIMvEtdSVHJF5oPhhFIWihkdHzd0pH4Z5gvHRn2NupsD55Y3DvHpCb7i v79j6eGYq9o7CZIIw6iEmzbmmRCREDZBOlwUD1Z9Pb976x4zEsy5UOqv8LYnwaakzOQY IirD3A5qbNGeQeu4HEY36JD3TVcWlkdG6KvChHw4HuTih5/tcr3r689cAKelLorI+M5B 9z+w== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 140.77.167.222 is neither permitted nor denied by domain of gaetan....@ens-lyon.fr) smtp.mailfrom=gaetan....@ens-lyon.fr Return-Path: Received: from labbe.ens-lyon.fr (labbe.ens-lyon.fr. [140.77.167.222]) by gmr-mx.google.com with ESMTP id n128si903192wmn.1.2017.07.18.08.28.38 for ; Tue, 18 Jul 2017 08:28:38 -0700 (PDT) Received-SPF: neutral (google.com: 140.77.167.222 is neither permitted nor denied by domain of gaetan....@ens-lyon.fr) client-ip=140.77.167.222; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 140.77.167.222 is neither permitted nor denied by domain of gaetan....@ens-lyon.fr) smtp.mailfrom=gaetan....@ens-lyon.fr Received: from localhost (localhost [127.0.0.1]) by labbe.ens-lyon.fr (Postfix) with ESMTP id 6A20D320849 for ; Tue, 18 Jul 2017 17:26:59 +0200 (CEST) X-Virus-Scanned: by amavisd-new-2.10.1 (20141025) (Debian) at ens-lyon.fr Received: from labbe.ens-lyon.fr ([127.0.0.1]) by localhost (labbe.ens-lyon.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id T-FkLWnPA1ge for ; Tue, 18 Jul 2017 17:26:58 +0200 (CEST) Received: from [172.28.34.14] (unknown [193.52.83.10]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (Client did not present a certificate) by labbe.ens-lyon.fr (Postfix) with ESMTPSA id 62B5F320A00 for ; Tue, 18 Jul 2017 17:26:56 +0200 (CEST) Subject: Re: [HoTT] Non-enumerability of R To: HomotopyTypeTheory@googlegroups.com References: From: Gaetan Gilbert Message-ID: Date: Tue, 18 Jul 2017 17:28:34 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US 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 > > 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 > . > > > -- > 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.