Re: [HoTT] Is synthetic the right word?

[Andrej Bauer <andrej...@andrej.com>]

Various subjects have been called synthetic, and in every case I am
aware of the subject develops a branch of mathematics in (the internal
language of) a topos that is particularly suitable for the topic at
hand. Thus we have had Synthetic Differential Geometry, Synthetic
Domain Theory, Synthetic Topology and Synthetic Computability.

The word "synthetic" here refers to the fact that we create an
artificial, or synthetic, world of mathematics suitable for doing
whatever it is we are doing. For instance, the effective topos is
suitable for doing computability. If I am wrong about this particular
point, I would like to hear why Synthetic Differential Geometry was
originally so called.

The word "synthetic" does not refer to there being a completely new
thing that is different from what has been done so far. In the above
examples there is always a clear connection to the traditional ways,
with suitable transfer theorems guaranteeing that the synthetic world
is not just a hallucination.

In line with the established terminology, such as it may be, Synthetic
Homotopy Theory would be homotopy theory developed in (the internal
language of) a topos, or other suitable structure, that is
particularly suitable for doing homotopy theory. One may put a varying
amounts of emphasis on the internal language or the models, according
to taste. What I think we are lacking at the moment is a clear way of
transfering results in synthetic homotopy theory back to a traditional
setup. The explanation which says "interpretet in Kan simplicial sets
and apply the geometric realization" does not seem to be good enough,
or at least it should be made mathematically precise. Perhaps the we
should just forget about topology and use simplicial sets as the
natural traditional setup for doing homotopy theory?

We even have Synthetic Combinatorics, although its author prefers to
adopt terminology from biology and anthropology :-)

With kind regards,

Andrej