From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.63.11 with SMTP id m11mr114624wma.17.1500364496199; Tue, 18 Jul 2017 00:54:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.158.146 with SMTP id h140ls453532wme.2.gmail; Tue, 18 Jul 2017 00:54:55 -0700 (PDT) X-Received: by 10.28.153.206 with SMTP id b197mr115982wme.12.1500364495061; Tue, 18 Jul 2017 00:54:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500364495; cv=none; d=google.com; s=arc-20160816; b=lquDH/1z4GGTmh7uHTbHCWkjh4f9IyoJXZSFN28DEnh/BJ6cPnlxWs4GfQvsvJ1rEr UdGztyU1pYdQ+lOwOYuIB15URK70UlzWQWB1xbVgZbxtWwLhbwF8prCMVqXrW7iiHTCT HlByh1aStBb6TQmUqzxMfHUJT2y1HBmaSr4vvYbORBJMZ4ukF04aa4fdA3yZHrWByZbO gANiGdyXce/u6nK9/0MLxjqjcA+dj8G3vhhM4Loq14gQvpYeGIW4hijLXC3RF+1As6RR XdGQ1xLhybh+HdZUbfO/CcntUpvbZCLx1ngQtwrAL3YMJM8jrapCtJohlN4yG1iGPIXJ 5OgQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-transfer-encoding :content-disposition:mime-version:references:message-id:subject:cc :to:from:date:arc-authentication-results; bh=xkkCYKonEDQpH41w/4aOxYie3HZMsKBGsYgxxCtswNI=; b=OUKBa11V5Rw/GbvOQwbxcRk9GrJ4qLRyuW/GZ6D2aC45oPPIsrh9/s8K9lAvHm+2Z8 qubR2Betf+TNxP097MRFbgHWIePhNE63PJlsQOEhNV/7SxD/PP4mdV6ZL65BcQPkfIlU JwZ5C0+rLFDeLuQySptpqVTuk5zd+rdnYUxTDXAQUCiztEsjTU2tF387WsG0P788h/v2 qPVWkctmcKWdZ6urJ3cSTUksNxNyoaHDYpSRXyxS4ALrlEAN3Y20L+uodL2XsRIf2Igj vPU3XNqLRpiH9qVqwVIOFPurC70ootrO2yFXlYl7ovqdFZKNIfamV4iKe894poc3To8W mikg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.232 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (lnx503.hrz.tu-darmstadt.de. [130.83.156.232]) by gmr-mx.google.com with ESMTPS id q8si1610401wmg.3.2017.07.18.00.54.54 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 18 Jul 2017 00:54:54 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.232 as permitted sender) client-ip=130.83.156.232; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.232 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v6I7sr9r007025; Tue, 18 Jul 2017 09:54:53 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v6I7srRF010930; Tue, 18 Jul 2017 09:54:53 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 625261A3D7F; Tue, 18 Jul 2017 09:54:55 +0200 (CEST) Date: Tue, 18 Jul 2017 09:54:55 +0200 From: Thomas Streicher To: Andrej Bauer Cc: Homotopy Type Theory Subject: Re: [HoTT] Non-enumerability of R Message-ID: <20170718075455.GB8604@mathematik.tu-darmstadt.de> References: <3215aa4a-789c-4d2b-b0ee-a546c5a99152@googlegroups.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.7.18.74816 X-PMX-RELAY: outgoing On Mon, Jul 17, 2017 at 03:52:28PM +0200, Andrej Bauer wrote: > > In fact, no appeal to Stone-Weierstraß is needed, because that one is > > about *uniform* approximation of functions, whereas we only need local > > approximation. Yes? > > It's still easier than that, isn't it already the case that the > constant functions taking a rational value suffice? On every open > interval every continuous map intersects one of those. At www.mathematik.tu-darmstadt.de/~streicher/rnc.pdf you find a littele note of mine where I fill in some details in the Rosolini-Spitters argument that Sh(R) doesn't validate the statement that for every sequenc a in R^D there is a b in R^D with b # a_n for all n (# stands for "apart"). But this argument doesn't show that \neg \exists a : N -> R. \forall b : R. \exists n:N. a_n = b fails in Sh(R). I don't know any topos where this fails. Thomas