From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.37.137 with SMTP id q9mr3365234ota.6.1466080670409; Thu, 16 Jun 2016 05:37:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.34.47 with SMTP id k44ls1501569qgk.54.gmail; Thu, 16 Jun 2016 05:37:49 -0700 (PDT) X-Received: by 10.237.37.220 with SMTP id y28mr3309615qtc.2.1466080669926; Thu, 16 Jun 2016 05:37:49 -0700 (PDT) Return-Path: Received: from smtp.andrew.cmu.edu (SMTP.ANDREW.CMU.EDU. [128.2.105.203]) by gmr-mx.google.com with ESMTPS id x68si2182290ywd.6.2016.06.16.05.37.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 05:37:49 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of awo...@cmu.edu designates 128.2.105.203 as permitted sender) client-ip=128.2.105.203; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of awo...@cmu.edu designates 128.2.105.203 as permitted sender) smtp.mailfrom=awo...@cmu.edu Received: from [192.168.0.15] (c83-253-111-143.bredband.comhem.se [83.253.111.143]) (user=awodey mech=PLAIN (0 bits)) by smtp.andrew.cmu.edu (8.15.2/8.15.1) with ESMTPSA id u5GCbkAp102968 (version=TLSv1 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Thu, 16 Jun 2016 08:37:48 -0400 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Is synthetic the right word? From: Steve Awodey In-Reply-To: Date: Thu, 16 Jun 2016 14:37:45 +0200 Cc: =?utf-8?Q?=22Joyal=2C_Andr=C3=A9=22?= , Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> To: =?utf-8?Q?andr=C3=A9_hirschowitz?= X-Mailer: Apple Mail (2.2104) X-PMX-Version: 6.3.0.2556906, Antispam-Engine: 2.7.2.2107409, Antispam-Data: 2016.3.29.90917 X-SMTP-Spam-Clean: 9% ( MULTIPLE_RCPTS 0.1, HTML_00_01 0.05, HTML_00_10 0.05, MIME_LOWER_CASE 0.05, SUPERLONG_LINE 0.05, BODYTEXTP_SIZE_3000_LESS 0, BODY_SIZE_1600_1699 0, BODY_SIZE_2000_LESS 0, BODY_SIZE_5000_LESS 0, BODY_SIZE_7000_LESS 0, FROM_EDU_TLD 0, IN_REP_TO 0, LEGITIMATE_NEGATE 0, MSG_THREAD 0, MULTIPLE_RCPTS_RND 0, NO_URI_HTTPS 0, RDNS_GENERIC_POOLED 0, RDNS_SUSP 0, RDNS_SUSP_GENERIC 0, REFERENCES 0, __ANY_URI 0, __BOUNCE_CHALLENGE_SUBJ 0, __BOUNCE_NDR_SUBJ_EXEMPT 0, __C230066_P2 0, __CT 0, __CTE 0, __CT_TEXT_PLAIN 0, __HAS_CC_HDR 0, __HAS_FROM 0, __HAS_MSGID 0, __HAS_X_MAILER 0, __IN_REP_TO 0, __MIME_TEXT_ONLY 0, __MIME_VERSION 0, __MSGID_APPLEMAIL 0, __MULTIPLE_RCPTS_CC_X2 0, __PHISH_SPEAR_STRUCTURE_1 0, __REFERENCES 0, __SANE_MSGID 0, __SUBJ_ALPHA_NEGATE 0, __TO_MALFORMED_2 0, __URI_NO_WWW 0, __URI_NS , __USER_AGENT_APPLEMAIL 0, __X_MAILER_APPLEMAIL 0) X-SMTP-Spam-Score: 9% X-Scanned-By: MIMEDefang 2.78 on 128.2.105.203 Dear Andre=E2=80=99 H., > On Jun 16, 2016, at 10:56 AM, andr=C3=A9 hirschowitz wrot= e: ... > When speaking about Guillaume's work, you may want to stress that his res= ult is completely new, because his sphere is not the classical sphere, and = not even a shadow of the classical sphere in any reasonable sense. You coul= d call it the synthetic sphere, or find a better wording. But a name is cle= arly needed for this new sphere and for this new homotopy theory. I don=E2=80=99t think it=E2=80=99s correct to say that the spheres, etc., o= f HoTT are new spheres. They are exactly the same spheres, only reasoned a= bout in a new way. The proofs are different in some respects, but also the= same in other respects. We are proving the same theorems, not new ones, u= sing different methods of proof. The interpretation of HoTT into axiomatic (categorical) homotopy theory, an= d then in turn into sSets, Top, etc., show that it is one subject =E2=80=94= homotopy theory. But each degree of abstraction also expands the subject.= In HoTT, one main difference is that the notion of a path, or a space, is = taken as primive, rather than being analyzed into a sequence, or set, of po= ints with some further structure. This difference is what we tried to desc= ribe with the term =E2=80=9Csynthetic=E2=80=9D. Maybe we should put some mo= re effort into explaining the choice of terminology, as the first round of = papers start coming out for publication. That makes a discussion such as t= his one timely and useful =E2=80=94 thanks for starting it! Regards, Steve