From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.51.149 with SMTP id z143mr4246534ywz.55.1466094482280; Thu, 16 Jun 2016 09:28:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.43.77 with SMTP id f13ls485606otd.35.gmail; Thu, 16 Jun 2016 09:28:01 -0700 (PDT) X-Received: by 10.157.27.240 with SMTP id v45mr504789otv.21.1466094481745; Thu, 16 Jun 2016 09:28:01 -0700 (PDT) Return-Path: Received: from data.hamecon.telecom.uqam.ca (data.hamecon.telecom.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id x68si2242787ywd.6.2016.06.16.09.28.01 for ; Thu, 16 Jun 2016 09:28:01 -0700 (PDT) Received-SPF: pass (google.com: domain of JOYAL...@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of JOYAL...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca Authentication-Results: data2.hamecon.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@MISSIVE.gst.uqam.ca Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postm...@MISSIVE.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@MISSIVE.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DRbgwcwZv_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3DSgJDDHH=5FwjgA=3A10_a=3DN659UExz7-8A=3A10_a=3DpD=5Fry4oyN?= =?us-ascii?q?xEA=3A10_a=3D4RBUngkUAAAA=3A8?= =?us-ascii?q?_a=3D1XWaLZrsAAAA=3A8_a=3DKS1XgwwmkbrNtz5H=5FkoA=3A9_a=3DpILNO?= =?us-ascii?q?xqGKmIA=3A10?= =?us-ascii?q?_a=3Dc4S9Whzb7AQA=3A10_a=3D=5FsbA2Q-Kp09kWB8D3iXc=3A22_a=3DnJc?= =?us-ascii?q?Ew6yWrPvoIXZ49MH8=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2APBwDz0mJX/9H20IReDoMwVn0Ggza5G?= =?us-ascii?q?RcHhXkCgSw8EAEBAQEBAQFlJ0ESAYN3AQEBBE4rEAIBCA0EBAEBAQokMQEdCAI?= =?us-ascii?q?ECAYBBAEHFQSIDw7ANQEBAQEBAQEBAQEBAQEBAQEBAQEBARcFinSEEhEBHoMqg?= =?us-ascii?q?i8FmHGGBZIAhUaPdTUfgggcgRE7bgeGa4FdNgF+AQEB?= X-IPAS-Result: =?us-ascii?q?A2APBwDz0mJX/9H20IReDoMwVn0Ggza5GRcHhXkCgSw8EAE?= =?us-ascii?q?BAQEBAQFlJ0ESAYN3AQEBBE4rEAIBCA0EBAEBAQokMQEdCAIECAYBBAEHFQSID?= =?us-ascii?q?w7ANQEBAQEBAQEBAQEBAQEBAQEBAQEBARcFinSEEhEBHoMqgi8FmHGGBZIAhUa?= =?us-ascii?q?PdTUfgggcgRE7bgeGa4FdNgF+AQEB?= X-IronPort-AV: E=Sophos;i="5.26,481,1459828800"; d="scan'208";a="142073739" Received: from unknown (HELO MISSIVE.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 16 Jun 2016 12:28:00 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.160]) by MISSIVE.gst.uqam.ca ([169.254.4.245]) with mapi id 14.02.0387.000; Thu, 16 Jun 2016 12:28:00 -0400 From: =?Windows-1252?Q?Joyal=2C_Andr=E9?= To: Michael Shulman CC: Homotopy Type Theory Subject: RE: [HoTT] Is synthetic the right word? Thread-Topic: [HoTT] Is synthetic the right word? Thread-Index: AQHRxzNfBKt/Gzdp2kOWcjgxaRfKUp/rB+7cgAEGkwCAAD3pgP//w3nbgABpQQD//8GE4Q== Date: Thu, 16 Jun 2016 16:28:00 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138B93899@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> <8C57894C7413F04A98DDF5629FEC90B138B9383F@Pli.gst.uqam.ca>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Michael, Quillen homotopical algebra is very good for working in an infty-category with finite limits and colimits, but it is not well adapted to exploit the = specific nature of an infty-topos. For this, we need a more powerful axiomatic syste= m. Axiomatic homotopy theory is what comes after Quillen homotopical algebra. Axiomatic infty-topos theory could be the main branch. One problem with the word "synthetic" is that it needs to be explained, and= possibly justified.=20 Synthetic differential geometry is not popular among differential geometers= .=20 The basic ideas are known and it is regarded with contempt. Sad. Best regards, Andr=E9 ________________________________________ From: Michael Shulman [shu...@sandiego.edu] Sent: Thursday, June 16, 2016 11:17 AM To: Joyal, Andr=E9 Cc: Homotopy Type Theory Subject: Re: [HoTT] Is synthetic the right word? The problem is that by now, "axiomatic homotopy theory" has come to essentially mean "Quillen model categories", so it gives no indication of how "homotopy theory in type theory" differs from that. I still do not see the problem with "synthetic". Many mathematicians are not familiar with the word in this context, but that's not a problem; we just explain what it means. Mathematicians are used to words having precise meanings that have to be explained before they can be understood. On Thu, Jun 16, 2016 at 8:03 AM, Joyal, Andr=E9 wrote: > Thank you all, > > I hope you will forgive me if I try to answer you all in one message. > > I understand the opposition between "synthetic" and "analytic" and I trul= y believe > that univalent type theory is bringing something new to homotopy theory. > But my concern is more sociological than philosophical. > Homotopy theory is a well established field of mathematics > and homotopy theorists are not stupid (no offense). > > J.H.C. Whitehead wrote in 1950: > > "The ultimate aim of algebraic homotopy is to construct a purely algebrai= c theory, > which is equivalent to homotopy theory in the same sort of way that =91an= alytic=92 is > equivalent to =91pure=92 projective geometry". > > A giant step in that direction was the creation of homotopical algebra > by Daniel Quillen (1967). > > The notion of Quillen model category enjoys many of the virtues attribute= d to homotopy type theory. > Also the notion of Brown fibration category. > It happens that the syntactic category of homotopy type theory > is a Brown fibration category (by a result of Avigad, Kapulkin and Lumsda= ine) > The notion of path object can be defined in any Brown fibration category. > The fact that spheres can constructed in homotopy type theory > (with higher inductive types) is not surprising, once the connection > between Martin-Lof type theory and homotopy theory is understood > (thanks to the work of Awodey and Warren). > > This been said, homotopy type theory offer a formal description of > important constructions in the homotopy theory of spaces and stacks. > The analogy with the theory of elementary toposes is striking, > since the latter is a categorical description of important constructions = in the theory of sets and sheaves. > The fact that formal logic can contribute to homotopy theory came as a su= rprise. > But is often the way mathematics advance. > > Homotopy type theory is presently in its infancy. > I hope it will keep growing but it is hard to predict the future directio= ns. > It should remain axiomatic. > Nicola Gambino has proposed "Axiomatic homotopy theory". > It is the line of a tradition and it leaves the future open. > > Best regards, > Andr=E9 > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.