From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.242.69 with SMTP id b66mr2724746ywf.24.1500299550597; Mon, 17 Jul 2017 06:52:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.11.224 with SMTP id 93ls476224iol.33.gmail; Mon, 17 Jul 2017 06:52:29 -0700 (PDT) X-Received: by 10.129.109.65 with SMTP id i62mr5593078ywc.77.1500299549328; Mon, 17 Jul 2017 06:52:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500299549; cv=none; d=google.com; s=arc-20160816; b=t3L1EPR3/DrRIuMdapLk8xPoZvo7JQa3SN/DXM40/Pbs7zrDGKvDx688/cXvplNdLE k02b22D16bYW2+/fGWqDjd5KQIxeW2gKYGXQ3XEQuARVSGV2P01GhyuZ9Fxm+d0B5hiZ dsJf90lhgN1nJWLedl/CIzzfceY6d9tkCC3fziIU+DE4SKqWhCnYaA2oGCVZD97n+yki e6ONZFbvsGpitaGWui4FXZI2tNoyhDYvXGt7DpPTyV3nJOGt8wEKw3HyR/Lm5Oy0hOOw 3I1LTOrUCDWhJKCLUFHGMzR7m0w29Jwm1yOcj846MjSWfLM7BL7exfzT+Avz1GyKlMbA +6Sw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=bMPt2lP212o7c/UNEQTyfUsU6jjPM+J6u1f+Tq3RB/Y=; b=BJ9Lrp14SUguU9bsxv0rIiTPLePYgqLkOoM2RkNcEmbDiAtafiEckT4zjKMHGJSyBS wPWv2G2oRoudcImH+8PQV09ux0aTEGpxeUvMsNqpzTjrn1XvXYU4yNf0Mfr4YllXK4a2 gzLicAuyfzdJyIDhCQ+OGx8tuVXOR8EorGyaV6hdhsuHblNzSlflPMBSaCitmkEb1CpS D8MVY8YWDQIQdeS6qanmXiWyusARKlzsNzIyGPz++BeW41MDEBznztaStQxu95LXk759 0iGTJROc83Ln0IVQkTfGZFDgjuPQ6QJV08ayZUMSM6ExyH1tXHti5Vg4Dlj4Pt6kztzk w9Xg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.b=jB/nXUhP; spf=neutral (google.com: 2607:f8b0:4002:c05::22d 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-x22d.google.com (mail-yw0-x22d.google.com. [2607:f8b0:4002:c05::22d]) by gmr-mx.google.com with ESMTPS id u128si1308184ywg.4.2017.07.17.06.52.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 17 Jul 2017 06:52:28 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c05::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.b=jB/nXUhP; spf=neutral (google.com: 2607:f8b0:4002:c05::22d is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yw0-x22d.google.com with SMTP id l21so47528640ywb.1 for ; Mon, 17 Jul 2017 06:52:28 -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:to :content-transfer-encoding; bh=bMPt2lP212o7c/UNEQTyfUsU6jjPM+J6u1f+Tq3RB/Y=; b=jB/nXUhP5m8zldPCg+5ndwHN+xyzsR0lF1Vh5zo+w9uKvXjNkTItPsZ3xbjsbn322R wyHh80D2IwBLZaeX5gScFKfNl4X3lcmnDlO1o4mOEH+DLZfI3eGLsfcB7FL95gmVzNeW kCUcINeodvckIpGUcQlaVZNpiNt7lrVRCQmLBwahKmcvxvqcXg22tqQ3UzVH2zmFmywI JKhh8b55XBrDHc1/pfzaBl2trPj31XXyI8Q58zrqsJT/+fG4F+8codYiWZIwUot+ByX4 7hY1hLqSV+IxjBl1cZc/0KvJCPAgqUhBjpucjw33vJjN/Lm+muuZlSDG8MOQ52WjJoTz rfEg== X-Gm-Message-State: AIVw111Fda4BL0a/vSyJYe13qQ2LUtQmTLkaD8XZbmsapr2kw0e0hp6Y aqc55lEZ7rogUqbXX8JpkiEc2hSJlOEj X-Received: by 10.129.183.31 with SMTP id v31mr7923699ywh.123.1500299548542; Mon, 17 Jul 2017 06:52:28 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.68.139 with HTTP; Mon, 17 Jul 2017 06:52:28 -0700 (PDT) In-Reply-To: References: <3215aa4a-789c-4d2b-b0ee-a546c5a99152@googlegroups.com> From: Andrej Bauer Date: Mon, 17 Jul 2017 15:52:28 +0200 Message-ID: Subject: Re: [HoTT] Non-enumerability of R To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > In fact, no appeal to Stone-Weierstra=C3=9F is needed, because that one i= s > 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.