From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.18.29 with SMTP id a29mr5582623ioj.6.1466107375200; Thu, 16 Jun 2016 13:02:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.185.131 with SMTP id j125ls780857iof.26.gmail; Thu, 16 Jun 2016 13:02:54 -0700 (PDT) X-Received: by 10.66.101.230 with SMTP id fj6mr5078540pab.15.1466107374467; Thu, 16 Jun 2016 13:02:54 -0700 (PDT) Return-Path: Received: from mail-vk0-x231.google.com (mail-vk0-x231.google.com. [2607:f8b0:400c:c05::231]) by gmr-mx.google.com with ESMTPS id v190si113216vkf.2.2016.06.16.13.02.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 13:02:54 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::231 as permitted sender) client-ip=2607:f8b0:400c:c05::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::231 as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x231.google.com with SMTP id u64so88370666vkf.3 for ; Thu, 16 Jun 2016 13:02:54 -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; bh=5xFohZVjNLXsrYSB7nE9aRYJC4WaITodiedjh/ap37k=; b=JOd/H41w6pE86gzmZNCYHTHxPY6d0PeK2JKhsgEBD6JG4MHdP2efy5dYbxgdpUA467 41LAivY+nEEedgMGl0V7kVj5wbZNqWNitEmodd+rJfcfQ9PvYpOscp4wnP4964+2u6JW 4eL8yrj18BkLmZyzBSLtIjKrsOU0TKytF8ibaIPvrdKDd+QrNPIH5bYnfPwx6E/Kz1CT +tWjDacQEb/N2yA8iFYp6tw2TQKocRYIrwJbggGQdBVUCkA00X5YaX0kk7OpWs4p4u1e 0LM10ve7BONHivZcm89FU/dNBnUCQigyzbX4KOHbeRa7sjyeAkz/NYd2IUuZz/OeXqky MaLQ== X-Gm-Message-State: ALyK8tJxB2617lMHStX5DevYm+VEx1H0Us7kIbEHvMqBAlAUA2nTd+KYNOb0T/+SM5nRnl3CS80j3DRtwHgrog== X-Received: by 10.31.200.196 with SMTP id y187mr2851374vkf.125.1466107374174; Thu, 16 Jun 2016 13:02:54 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.16.66 with HTTP; Thu, 16 Jun 2016 13:02:53 -0700 (PDT) In-Reply-To: <5762FB77.3080706@cs.bham.ac.uk> References: <5762889C.8080401@cs.bham.ac.uk> <5762FB77.3080706@cs.bham.ac.uk> From: Egbert Rijke Date: Thu, 16 Jun 2016 22:02:53 +0200 Message-ID: Subject: Re: [HoTT] Is synthetic the right word? To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a114846383d85e805356ab954 --001a114846383d85e805356ab954 Content-Type: text/plain; charset=UTF-8 My experience, and I'm only speaking for myself, is that I have never really needed to use terminology such as "synthetic homotopy theory" when doing HoTT. The terminology "homotopy type theory", which to me refers to the synergy of homotopy theoretic and type theoretic methods and ideas, suffices for me. In the HoTT book, the word "synthetic" was used either to contrast the synthetic method to the analytic method, or to emphasize the elementary nature of the proofs in Chapter 8. Phrases like "synthetic approach" have only appeared in the context of such an explanation, and not in isolation. Note that the phrase "synthetic homotopy theory" does not appear in the book. With kind regards, Egbert On Thu, Jun 16, 2016 at 9:18 PM, Martin Escardo wrote: > I sent this this morning only to Andrej this morning, which seems to > resonate with what people said later, in particular Nicola: > > ---- Thu, 16 Jun 2016 12:08:12 +0100 > Andrej, you forgot to include synthetic geometry in your list (which > doesn't need a topos). > > https://en.wikipedia.org/wiki/Synthetic_geometry > "Geometry, as presented by Euclid in the elements, is the quintessential > example of the use of the synthetic method." > > We probably regard the synthetic circle as in some sense the same as the > analytic circle - although if our synthetic geometry doesn't have enough > axioms, it may be talking about the circle of another world. > > And we make models of synthetic geometry in analytic geometry, but > synthetic geometry is intended to also stand on its own, without the > need of an analytical model. > > Isn't the synthetic method (that of primitive notions "defined" by > axioms) everywhere? Even set theory is like that (we start with the > undefined primitive notions of set and membership, and use axioms to try > to capture some intuition we may have - we never actually say what a set > "really" is, other than giving intuitions such as "collections"). > > Similarly, when we do classical analysis, we work with a complete > Archimedian field, and not with the Dedekind or Cauchy reals (which we > can use as analytic models of the complete Archimedian field in set > theory). > --/-- > > Now I add this: similarly, HoTT, UF or what-you-have, as some people > conceive, including myself, is intended to stand on its own, before we > consider any model, very much like Euclidean geometry. > > What Andre Joyal disputes (and I did too in the previous thread) is not > the philosophy (or: better, point of view) but rather whether the words > which we use to advertise all of this have unintended connotations which > invoke the unintended meanings more than the intended one. > > M. > > > > -- > 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. > --001a114846383d85e805356ab954 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
My experience, and I'm only speaking for mys= elf, is that I have never really needed to use terminology such as "sy= nthetic homotopy theory" when doing HoTT. The terminology "homoto= py type theory", which to me refers to the synergy of homotopy theoret= ic and type theoretic methods and ideas, suffices for me.

In the HoT= T book, the word "synthetic" was used either to contrast the synt= hetic method to the analytic method, or to emphasize the elementary nature = of the proofs in Chapter 8. Phrases like "synthetic approach" hav= e only appeared in the context of such an explanation, and not in isolation= . Note that the phrase "synthetic homotopy theory" does not appea= r in the book.

With kind regards,
Egbert

On Thu, Jun 16, 2016= at 9:18 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrot= e:
I sent this this morning only to Andre= j this morning, which seems to resonate with what people said later, in par= ticular Nicola:

----=C2=A0 Thu, 16 Jun 2016 12:08:12 +0100
Andrej, you forgot to include synthetic geometry in your list (which
doesn't need a topos).

https://en.wikipedia.org/wiki/Synthetic_geometry=
"Geometry, as presented by Euclid in the elements, is the quintessenti= al
example of the use of the synthetic method."

We probably regard the synthetic circle as in some sense the same as the analytic circle - although if our synthetic geometry doesn't have enoug= h
axioms, it may be talking about the circle of another world.

And we make models of synthetic geometry in analytic geometry, but
synthetic geometry is intended to also stand on its own, without the
need of an analytical model.

Isn't the synthetic method (that of primitive notions "defined&quo= t; by
axioms) everywhere? Even set theory is like that (we start with the
undefined primitive notions of set and membership, and use axioms to try to capture some intuition we may have - we never actually say what a set "really" is, other than giving intuitions such as "collectio= ns").

Similarly, when we do classical analysis, we work with a complete
Archimedian field, and not with the Dedekind or Cauchy reals (which we
can use as analytic models of the complete Archimedian field in set theory)= .
--/--

Now I add this: similarly, HoTT, UF or what-you-have, as some people concei= ve, including myself, is intended to stand on its own, before we consider a= ny model, very much like Euclidean geometry.

What Andre Joyal disputes (and I did too in the previous thread) is not the= philosophy (or: better, point of view) but rather whether the words which = we use to advertise all of this have unintended connotations which invoke t= he unintended meanings more than the intended one.

M.



--
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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114846383d85e805356ab954--