From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.29.150 with SMTP id d144mr1065957wmd.0.1466104696553; Thu, 16 Jun 2016 12:18:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.87 with SMTP id 84ls108759ljf.16.gmail; Thu, 16 Jun 2016 12:18:15 -0700 (PDT) X-Received: by 10.46.1.38 with SMTP id 38mr938448ljb.3.1466104695883; Thu, 16 Jun 2016 12:18:15 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id q124si600431wme.3.2016.06.16.12.18.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 12:18:15 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of m.es...@cs.bham.ac.uk designates 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of m.es...@cs.bham.ac.uk designates 147.188.128.150 as permitted sender) smtp.mailfrom=m.es...@cs.bham.ac.uk Received: from [147.188.128.127] (helo=bham.ac.uk) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1bDcnv-0002X6-OS for HomotopyT...@googlegroups.com; Thu, 16 Jun 2016 20:18:15 +0100 Received: from host81-147-122-132.range81-147.btcentralplus.com ([81.147.122.132] helo=[192.168.1.112]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bDcnv-00009T-Ea for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Thu, 16 Jun 2016 20:18:15 +0100 Subject: Re: [HoTT] Is synthetic the right word? References: <5762889C.8080401@cs.bham.ac.uk> To: "HomotopyT...@googlegroups.com" From: Martin Escardo Organization: University of Birmingham Message-ID: <5762FB77.3080706@cs.bham.ac.uk> Date: Thu, 16 Jun 2016 20:18:15 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0 MIME-Version: 1.0 In-Reply-To: <5762889C.8080401@cs.bham.ac.uk> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) 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.