Re: [HoTT] Is synthetic the right word?

[Urs Schreiber <urs.sc...@googlemail.com>]

> It is "the same" in the standard model, but the theorem in HoTT gives
> a more general result than the one in classical homotopy.

Indeed, and this is usefully compared to the original use of
"synthetic" in "synthetic geomety":

Euclid's synthetic axioms for geometry (without the parallel axiom)
were thought to apply only to classical flat Euclidean space. The
surprise was immense when it was realized that the same synthetic
geometry has interpretation also in hyperbolic geometry and in
elliptic geometry.

That is the prospect of synthetic homotopy theory: to be for homotopy
theory what the generalization from flat to curved spaces has been for
geometry.