From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.140.43.3 with SMTP id d3mr3785105qga.5.1466089410678; Thu, 16 Jun 2016 08:03:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.31.181 with SMTP id f50ls1654500qgf.50.gmail; Thu, 16 Jun 2016 08:03:30 -0700 (PDT) X-Received: by 10.140.85.42 with SMTP id m39mr3869257qgd.13.1466089410223; Thu, 16 Jun 2016 08:03:30 -0700 (PDT) Return-Path: Received: from data.crochet.telecom.uqam.ca (mail3.uqam.ca. [132.208.246.162]) by gmr-mx.google.com with ESMTP id y11si121708itf.2.2016.06.16.08.03.29 for ; Thu, 16 Jun 2016 08:03:30 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.162 as permitted sender) client-ip=132.208.246.162; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.162 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca Authentication-Results: data2.crochet.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@Message.gst.uqam.ca Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.crochet.telecom.uqam.ca: no sender authenticity information available from domain of postm...@Message.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.crochet.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@Message.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DTPHlMwRa_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?= =?us-ascii?q?_a=3D-hd6UOgr-SX-JIobzGAA=3A9_a=3DpILNOxqGKmIA=3A10?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2AFBwB/vmJX/9H20IRegz6BWbxPhhcCg?= =?us-ascii?q?Sg8EAEBAQEBAQFlJ0ESAYN4AQEEgQkCAQgNFSQyJQIEG4gowCoMJYp0hEKDKoI?= =?us-ascii?q?vBZhxmAWFRo91NR+CCByBTIdgghMBfgEBAQ?= X-IPAS-Result: =?us-ascii?q?A2AFBwB/vmJX/9H20IRegz6BWbxPhhcCgSg8EAEBAQEBAQF?= =?us-ascii?q?lJ0ESAYN4AQEEgQkCAQgNFSQyJQIEG4gowCoMJYp0hEKDKoIvBZhxmAWFRo91N?= =?us-ascii?q?R+CCByBTIdgghMBfgEBAQ?= X-IronPort-AV: E=Sophos;i="5.26,480,1459828800"; d="scan'208";a="162370780" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.crochet.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 16 Jun 2016 11:03:29 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.160]) by Message.gst.uqam.ca ([169.254.1.94]) with mapi id 14.02.0387.000; Thu, 16 Jun 2016 11:03:29 -0400 From: =?Windows-1252?Q?Joyal=2C_Andr=E9?= To: 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//w3nb Date: Thu, 16 Jun 2016 15:03:28 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138B9383F@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> ,<2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> In-Reply-To: <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> 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 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 truly = believe=20 that univalent type theory is bringing something new to homotopy theory.=20 But my concern is more sociological than philosophical.=20 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 algebraic = theory,=20 which is equivalent to homotopy theory in the same sort of way that =91anal= ytic=92 is=20 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 attributed = 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 Lumsdain= e) 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=20 between Martin-Lof type theory and homotopy theory is understood (thanks to the work of Awodey and Warren).=20 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 surp= rise. 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 directions= . 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