Re: [HoTT] Is synthetic the right word?

[Martin Escardo <m.es...@cs.bham.ac.uk>]

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.