From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.222.197 with SMTP id qo5mr1170095pac.44.1466032391765; Wed, 15 Jun 2016 16:13:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.22.70 with SMTP id 67ls474319iow.5.gmail; Wed, 15 Jun 2016 16:13:11 -0700 (PDT) X-Received: by 10.36.85.196 with SMTP id e187mr1708296itb.2.1466032391149; Wed, 15 Jun 2016 16:13:11 -0700 (PDT) Return-Path: Received: from data.crochet.telecom.uqam.ca (data.crochet.telecom.uqam.ca. [132.208.246.162]) by gmr-mx.google.com with ESMTP id c2si2225668ywf.5.2016.06.15.16.13.10 for ; Wed, 15 Jun 2016 16:13:11 -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=3DpD=5Fry4oyNxEA=3A10_a=3D4RBUngkUA?= =?us-ascii?q?AAA=3A8_a=3DpGLkceISAAAA=3A8?= =?us-ascii?q?_a=3D1XWaLZrsAAAA=3A8_a=3DrXWxeoHxe1hCXQpiz-8A=3A9_a=3D8FsqdIi?= =?us-ascii?q?bnht3joY2=3A21?= =?us-ascii?q?_a=3DP3Ch0VOkLDZ99JfT=3A21_a=3DwPNLvfGTeEIA=3A10_a=3Dc4S9Whzb7?= =?us-ascii?q?AQA=3A10?= =?us-ascii?q?_a=3DBRmS=5FEO94s2elpuwieEA=3A9_a=3D7ehrcpj45-UpqPfF=3A21_a=3D?= =?us-ascii?q?=5FaCiIjXfUFcYr1Dt=3A21?= =?us-ascii?q?_a=3DKjc4oDzQfs953OhF=3A21_a=3D=5FW=5FS=5F7VecoQA=3A10_a=3Dfrz?= =?us-ascii?q?4AuCg-hUA=3A10?= =?us-ascii?q?_a=3D=5FsbA2Q-Kp09kWB8D3iXc=3A22_a=3D6kGIvZw6iX1k4Y-7sg4=5F=3A?= =?us-ascii?q?22_a=3DnJcEw6yWrPvoIXZ49MH8=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2BvBQCO4GFX/9H20IRdgnBOVn0GgzarL?= =?us-ascii?q?o18FwEGhXkCgS47EQEBAQEBAQFlJ4RLAQEBBE47AgEIDQQEAQELHQchEAEUCQg?= =?us-ascii?q?CBAEHBwQBBwwJBId1AxcOu08Ng2QBAQEBAQEEAQEBAQEBAQEBGQWKdIJDgU8RA?= =?us-ascii?q?R40gnaCLwWNcTiKDDSGBYYpAYtWhUaIB4dtNCCDb24HiD0PFwMcAX4BAQE?= X-IPAS-Result: =?us-ascii?q?A2BvBQCO4GFX/9H20IRdgnBOVn0GgzarLo18FwEGhXkCgS4?= =?us-ascii?q?7EQEBAQEBAQFlJ4RLAQEBBE47AgEIDQQEAQELHQchEAEUCQgCBAEHBwQBBwwJB?= =?us-ascii?q?Id1AxcOu08Ng2QBAQEBAQEEAQEBAQEBAQEBGQWKdIJDgU8RAR40gnaCLwWNcTi?= =?us-ascii?q?KDDSGBYYpAYtWhUaIB4dtNCCDb24HiD0PFwMcAX4BAQE?= X-IronPort-AV: E=Sophos;i="5.26,478,1459828800"; d="scan'208,217";a="162287316" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.crochet.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 15 Jun 2016 19:13:09 -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; Wed, 15 Jun 2016 19:13:09 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: =?iso-8859-1?Q?andr=E9_hirschowitz?= , "Homotopy Type Theory" Subject: RE: [HoTT] Is synthetic the right word? Thread-Topic: [HoTT] Is synthetic the right word? Thread-Index: AQHRxzNfBKt/Gzdp2kOWcjgxaRfKUp/rB+7c Date: Wed, 15 Jun 2016 23:13:08 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138B93747@Pli.gst.uqam.ca> References: 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: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B138B93747Pligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B138B93747Pligstuqamca_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Dear Andr=E9 H, I was nice to meet you this afternoon and to be present at the Phd defense = of Guillaume Brunerie. I am very impressed by Brunerie's mastership in computing non-trivial homot= opy groups of spheres using exclusively the rules of homotopy type theory. This afternoon, I have expressed my opposition to calling homotopy type the= ory "Synthetic Homotopy Theory". You have expressed the desire to have a public discussion on this subject. I will try to be clear and short. The word "synthetic" suggests that a new kind of homotopy theory is born, something that is changing the fabric of homotopy theory itself. I disagree= . This is not to diminish the importance of the work of Voevodsky, Shulman, L= umsdane, Licata, Finster and Brunerie, on the contrary. Their work is original and absolutly= beautiful. But the contribution of homotopy type theory to homotopy theory is presently like the contribution of a stream to the flow of a river. The stream may grow in time and eventually become the main stream, but we a= re not there yet! Also, the water from the stream mixes very well with the water of the river= . It is building on classical concepts: fibrations, homotopy pullback, homotopy pushout, homotopy fiber, suspension, loop space, connected space, discrete space, classifying space, Freudenthal suspension theorem, Blakers-Massey theorem, Eilenberg-MacLane spaces. The "synthetic" label can make believe that the water from the stream has a different nature. I find it divisive. Homotopy type theory is the union of type theory with homotopy theory. To divide is the last thing we need. Best regards, Andr=E9 J ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of andr=E9 hirschowitz [mphm...@gmail.com] Sent: Wednesday, June 15, 2016 2:26 PM To: Homotopy Type Theory Subject: [HoTT] Is synthetic the right word? Hi, Today, I have discovered that some (nice) members of this community do not = like the word "synthetic" in the formula "Synthetic Homotopy Theory" used = in this group to name you know what. My opinion is that people working is this area deserve an accepted name for= this activity. So I consider that who finds this wording inadequate should= either argue HERE and NOW, or shut down forever (on this precise topic!)= . So? 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 e= mail to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --_000_8C57894C7413F04A98DDF5629FEC90B138B93747Pligstuqamca_ Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable
Dear Andr=E9 H,

I was nice to meet you this afternoon and to be present at the Phd defense = of Guillaume Brunerie.
I am very impressed by Brunerie's mastership in computing non-trivial homot= opy groups of spheres
using exclusively the rules of homotopy type theory.

This afternoon, I have expressed my opposition to calling homotopy type the= ory
"Synthetic Homotopy Theory". You have expressed the desire
 to have a public discussion on this subject.

I will try to be clear and short.
The word "synthetic" suggests that a new kind of homotopy theory = is born,
something that is changing the fabric of homotopy theory itself. I disagree= .
This is not to diminish the importance of the work of Voevodsky, Shulman, L= umsdane, Licata,
Finster and Brunerie, on the contrary. Their work is original and absolutly= beautiful.
 But the contribution of homotopy type theory to homotopy theory
is presently like the contribution of a stream to the flow of a river.
The stream may grow in time and eventually become the main stream, but we a= re not there yet!
Also, the water from the stream mixes very well with the water of the river= .
It is building on classical concepts: fibrations, homotopy pullback,
homotopy pushout, homotopy fiber, suspension, loop space, connected space,<= br> discrete space, classifying space, Freudenthal suspension theorem,
Blakers-Massey theorem, Eilenberg-MacLane spaces.
The "synthetic" label can make believe that the water
from the stream has a different nature. I find it divisive.
Homotopy type theory is the union of type theory with homotopy theory.
To divide is the last thing we need.

Best regards,
Andr=E9 J



From: homotopyt...@googlegroups.com [homo= topyt...@googlegroups.com] on behalf of andr=E9 hirschowitz [mphm...@gmail.= com]
Sent: Wednesday, June 15, 2016 2:26 PM
To: Homotopy Type Theory
Subject: [HoTT] Is synthetic the right word?

Hi,

Today, I have discovered that some (nice) members of this community do not = like the word "synthetic" in the formula  "Synthetic Ho= motopy Theory" used in this group to name you know what.

My opinion is that people working is this area deserve an accepted name for= this activity. So I consider that who finds this wording inadequate should= either  argue HERE  and NOW, or shut down forever (on this preci= se topic!).

So?

andr=E9

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--_000_8C57894C7413F04A98DDF5629FEC90B138B93747Pligstuqamca_--