From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.29.149 with SMTP id d143mr2940439wmd.4.1466086052310; Thu, 16 Jun 2016 07:07:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.213.195 with SMTP id m186ls75365lfg.98.gmail; Thu, 16 Jun 2016 07:07:31 -0700 (PDT) X-Received: by 10.25.217.213 with SMTP id s82mr718560lfi.9.1466086051623; Thu, 16 Jun 2016 07:07:31 -0700 (PDT) Return-Path: Received: from mail-wm0-x22d.google.com (mail-wm0-x22d.google.com. [2a00:1450:400c:c09::22d]) by gmr-mx.google.com with ESMTPS id f4si598124wmg.0.2016.06.16.07.07.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 07:07:31 -0700 (PDT) Received-SPF: pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::22d as permitted sender) client-ip=2a00:1450:400c:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::22d as permitted sender) smtp.mailfrom=mphm...@gmail.com Received: by mail-wm0-x22d.google.com with SMTP id v199so192279965wmv.0 for ; Thu, 16 Jun 2016 07:07:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=0Y96hFI+mZTGvn3FQTRORJRgvIdFUyUFyYV5d0d6Zcw=; b=Opeu61jrty+J3QLJAwaCjGVSbVXNaSTjJwqoGrb0pwZtWfVmUD9ByXjjJxWATlWbmF +YLeFHbORmegfMAN0LRHzwYGQwKruiKYJhjsiFQzxtnWxpuYkAZbMEQ0TnLnKNda4or2 x3L+x3FEPV6ZpdKqeJW/xTzFd/MH43MXAx9aQoz3/978SRP0MWYYZFN7DaAFLbPXhEFh ltqbAF3zigMIqdXgCOUKiJjK+HxwzxNR1sy21fvep9dNow4wmELvbRF8ayvhENlVGRkn J7SDfkKmoCInGMCYFzOEaGRkxNcOUn4m+Lm+r9yD5SjV5rH1K6kkSV8NCbjhAJQ9okT+ EgHQ== X-Gm-Message-State: ALyK8tKz7ScTq2oV4M1LTtey8j+4UcaC1G0+saZ39XtJuY/GYVU51xJVUI3D2NB3e7EZrUSrsmLetElD3f0XhA== X-Received: by 10.194.120.167 with SMTP id ld7mr880592wjb.69.1466086051241; Thu, 16 Jun 2016 07:07:31 -0700 (PDT) MIME-Version: 1.0 Sender: mphm...@gmail.com Received: by 10.194.112.33 with HTTP; Thu, 16 Jun 2016 07:07:11 -0700 (PDT) In-Reply-To: References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> From: =?UTF-8?Q?andr=C3=A9_hirschowitz?= Date: Thu, 16 Jun 2016 16:07:11 +0200 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: Andrej Bauer Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary=089e0115ff304b766c053565c247 --089e0115ff304b766c053565c247 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi! 2016-06-16 15:15 GMT+02:00 Andrej Bauer : > So at least at this level it > is a bit pointless to discuss things in absolute terms. The HoTT > proofs are *also* about the usual spheres. > I disagree with this formulation. It is not at all pointless (with respect to positions, publications and the like) to make clear in which sense synthetic spheres strictly encompass classical ones (and potentially "non-euclidian" future ones). And instead of stressing that these HoTT proofs are *also* about the usual spheres, we should rather stress that these HoTT proofs are *not at all only* about the usual spheres. andr=C3=A9 H --089e0115ff304b766c053565c247 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hi!

2016-06-16 15:15 GMT+02:00 Andrej B= auer <andrej...@andrej.com>:
So at least at this = level it
is a bit pointless to discuss things in absolute terms. The HoTT
proofs are *also* about the usual spheres.

<= div>

I disagree with this formulation. It is not at all pointless (with respect to positions, publications and the like) to make clear in which sense synthetic spheres strictly encompass classica= l ones (and=20 potentially "non-euclidian" future ones).

And instea= d of=20 stressing that these HoTT proofs are *also* about the usual spheres, we=20 should rather stress that these HoTT proofs are *not at all only* about=20 the usual spheres.

andr=C3=A9 H
=C2=A0


--089e0115ff304b766c053565c247--