From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.180.17 with SMTP id d17mr1802771iof.15.1466095939762; Thu, 16 Jun 2016 09:52:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.138.35 with SMTP id m35ls792471iod.79.gmail; Thu, 16 Jun 2016 09:52:19 -0700 (PDT) X-Received: by 10.66.254.199 with SMTP id ak7mr4295204pad.10.1466095939125; Thu, 16 Jun 2016 09:52:19 -0700 (PDT) Return-Path: Received: from mail-it0-x236.google.com (mail-it0-x236.google.com. [2607:f8b0:4001:c0b::236]) by gmr-mx.google.com with ESMTPS id o1si133054ith.1.2016.06.16.09.52.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 09:52:19 -0700 (PDT) Received-SPF: pass (google.com: domain of cgib...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) client-ip=2607:f8b0:4001:c0b::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of cgib...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) smtp.mailfrom=cgib...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x236.google.com with SMTP id a5so139975771ita.1 for ; Thu, 16 Jun 2016 09:52:19 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=cNl5bjFqEeLb3VYhYRc2F2Qjj/vUKAolzM+MpcQU+VM=; b=t5LlHejTqPQ/6HW2cdUFTwQ2/wP6XVIorWZ9ma+2m/g+0sq4CJxXNbN7raeJoQSY/G SJSOS350Dmdi6Nyq+uno+vxV2UkjBfe01PN0HjEDsisVpeZFz5cIlHLiwRpuj0qIHnfR q4iBSxKC+eHp5KwqpesjrMcwpMerS6dN4gW3bPPabCPJe1zMIYzMrSYkkzuezv6Z+BeL As/RoewZ0omipShxMTKhT+gRthAhbtkYA9fVIideG2Hbb3tHc9pOEd2p7RUS7F8oslBU CHUiVqx+dQPgaQv3Cpx4LAeeYkul3DAzhm22pkB97JEyj5YpB6+t5rquCocKP+7Zk2QM vu9w== X-Gm-Message-State: ALyK8tIdcd7UowfI7X86B3M3xHx/Lh/KYB/6Zs2PCITBEVGjJj3WGQ5rsmpKtuJsN0RIHDt0mhqlo2sFpCWskQ== X-Received: by 10.36.138.197 with SMTP id v188mr9622113itd.82.1466095938867; Thu, 16 Jun 2016 09:52:18 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.3.193 with HTTP; Thu, 16 Jun 2016 09:52:17 -0700 (PDT) In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B138B93899@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> <2850536B-0DB8-4F6D-AB3F-D5C28F6855B4@cmu.edu> <8C57894C7413F04A98DDF5629FEC90B138B9383F@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B138B93899@Pli.gst.uqam.ca> From: Cale Gibbard Date: Thu, 16 Jun 2016 12:52:17 -0400 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= Cc: Michael Shulman , Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable There is a certain irony in calling homotopy type theory "axiomatic", in that one of the major directions that people hope to develop it is to find nice axiom-free type theories (e.g. cubical type theory) in which univalence can be a theorem. But perhaps "axiomatic" is meant in a somewhat different sense there -- one which can include the introduction and elimination rules of the logic. On 16 June 2016 at 12:28, Joyal, Andr=C3=A9 wrote: > 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 th= e specific > nature of an infty-topos. For this, we need a more powerful axiomatic sys= tem. > 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, a= nd possibly justified. > Synthetic differential geometry is not popular among differential geomete= rs. > The basic ideas are known and it is regarded with contempt. Sad. > > Best regards, > Andr=C3=A9 > > ________________________________________ > From: Michael Shulman [shu...@sandiego.edu] > Sent: Thursday, June 16, 2016 11:17 AM > To: Joyal, Andr=C3=A9 > 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=C3=A9 wro= te: >> 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 tru= ly 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 algebra= ic theory, >> which is equivalent to homotopy theory in the same sort of way that =E2= =80=98analytic=E2=80=99 is >> equivalent to =E2=80=98pure=E2=80=99 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 attribut= ed 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 Lumsd= aine) >> 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 s= urprise. >> 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 directi= ons. >> 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=C3=A9 >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to a topic in the Go= ogle Groups "Homotopy Type Theory" group. > To unsubscribe from this topic, visit https://groups.google.com/d/topic/H= omotopyTypeTheory/B1upabJFHRc/unsubscribe. > To unsubscribe from this group and all its topics, send an email to Homot= opyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.