From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.101.85.4 with SMTP id f4mr15608241pgr.150.1500192568630; Sun, 16 Jul 2017 01:09:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.138.200 with SMTP id c69ls1713127ioj.23.gmail; Sun, 16 Jul 2017 01:09:27 -0700 (PDT) X-Received: by 10.129.91.4 with SMTP id p4mr11070202ywb.89.1500192567322; Sun, 16 Jul 2017 01:09:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500192567; cv=none; d=google.com; s=arc-20160816; b=ErmU9WoyXMyGldnZx7P2SGT4NfWcR9Ijjcsq5cRxBI2Jm8TMTze3Z21Q94A/aK6glt ptfuKq3H2EZaTn6AFQd1k9Yq3YWnXffXkwhuIVrE4ekjz9Csy4ZT7kIlFbMLFbaHuqZD zUWyhURa7NfBHX4k0K8P64y4Ls1H7Wl3wB6vF9zKiEzZ8ZmPdncRQ1vXVTR8OPTQCYTw s2Wdbg9/jilnnoxuAmoP/aKMoeHedlcLOah5suheriEUvniDUooVxi18dYM6F+OWqJOw cK5mwcSyLEbJK6YXX0M+i9BJ416G4FL5SyYR+py2SvLY2S2P8aXBkHtMMpPkx3W8uED4 v6JQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=HX3m4+7RYyX6rr6kV8HBwnk+9B22seOMh3dbx7BuX84=; b=R4Gb24B9rDi8cewfuAJfe6igJJdzc1gW6rSSv6853pCwiCsH66qAJWJWJD/hsu2o/V YSIknm2v0D8/62b/WjHmMpCp2Z6Y/AJKlxAZuX/wH8UPFJSpi/cIsASjPSk4hh8mzHiw 0Jtl6e21N5vlry85oO4yaG58USxRMpdTQHF2C5ggXpgfm4Hhfrab8Y7muuxtJ16cIsjg cqVX/TD4OA7ZMIVlW41WjW5yeFHQL8kBEyG/UdCbyaH5jZFWgVREyvra18qvJphyUBwt 0g2xW5iH0JwWjHTF6zW3/Y42HpIbVGN28M2oxl1yY+py3cODRHhCXvEeeAPaOj6wIJ9W 6juQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.b=c/SbvZ+9; spf=neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-yw0-x231.google.com (mail-yw0-x231.google.com. [2607:f8b0:4002:c05::231]) by gmr-mx.google.com with ESMTPS id q198si953417ywg.2.2017.07.16.01.09.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 16 Jul 2017 01:09:26 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c05::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.b=c/SbvZ+9; spf=neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yw0-x231.google.com with SMTP id v193so38229510ywg.2 for ; Sun, 16 Jul 2017 01:09:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:cc :content-transfer-encoding; bh=HX3m4+7RYyX6rr6kV8HBwnk+9B22seOMh3dbx7BuX84=; b=c/SbvZ+9FhDzbIajBiP241Q6DthQKCf19MhoOLFxXHloSeluXbyBFVWOi9nhxdT5ej oPnKlo9DSKjT+dhgauVRHwUkvrkind57Uerpg04UQqYp1i1sMz0qRnZPcqlBsWuT4cHz 14C4msDJBeVdPiRhV7r68ACMCKyh+SL72N+fzaqwKqXCnOEmUqw3LfL2rx9nFqFz6rUj XfAYdIrX8y7gRjeEf+VYBmPXybbufneY7NKx5pfZ5bpLjoHskCax1HJ9AcFJoCd5TlgX iEeVFBrQ75myNkJY0LIFsz8l3TQKpYQDNMuNSlMt6xALm8cd0JcOzPBkHss+usWNED7H qzBA== X-Gm-Message-State: AIVw113krRwGJED3VItjit593r9FWH5uta1D8vai0k2JKrqrdjBBr/Tq yNpYfPwr4NuciNBqON0zQi2UKvIjekI/ X-Received: by 10.129.165.71 with SMTP id c68mr12323779ywh.19.1500192566320; Sun, 16 Jul 2017 01:09:26 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.68.139 with HTTP; Sun, 16 Jul 2017 01:09:25 -0700 (PDT) In-Reply-To: <3215aa4a-789c-4d2b-b0ee-a546c5a99152@googlegroups.com> References: <3215aa4a-789c-4d2b-b0ee-a546c5a99152@googlegroups.com> From: Andrej Bauer Date: Sun, 16 Jul 2017 09:09:25 +0100 Message-ID: Subject: Re: [HoTT] Non-enumerability of R Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Andrew, thank you for your remarks. > 1. In the topos of sheaves over the closed unit interval the Dedekind rea= ls are not uncountable (in fact there is a countably enumerable "double neg= ation dense set" in the reals). I think it's reasonable to expect the same = thing in Thierry Coquand's cubical stack model and so show the same is cons= istent with HoTT. For the uninitiated, let me just clarify that one such not-not-dense countable subset is the set P of polynomials with rational coefficients. One then appeals to density of this set by the Stone-Weierstra=C3=9F theorem: for every continuous function on every open set there is some polynomial in P which intersects its graph, hence R \ P is empty. Let us call a set/object/type X *inexhaustible* when for every sequence a : N =E2=86=92 X there is some x in X which is different from all terms of the sequence. An inexhaustible set clearly is not countable. What your remark shows is that the reals cannot be shown to be inexhaustible in intuitionistic logic without choice. > 2. I would conjecture that constructing cubical sets internally in the in= finite time Turing machine topos gives a model of HoTT with an injection fr= om the reals to the naturals. Yes, but note by your third remarks, that as soon as there is an injection from reals to natural numbers, there can be no surjection going the other way. So cubical sets in infinite-time HoTT won't resolve the question. > 3. There is an entirely constructive proof that there is no bijection bet= ween the naturals and the reals (for any reasonable definition of real): fi= rst if there is an injection then the reals have decidable equality, but th= en this yields a proof that there is no surjection by a standard diagonal a= rgument. Neat. With kind regards, Andrej