Re: [HoTT] Is synthetic the right word?

[Cale Gibbard <cgib...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 707 bytes --]

In a similar but somewhat older vein we also have "synthetic geometry", referring to the sort of geometry where figures such as lines and circles, rather than being assembled as sets of points, are instead primitive notions.

Homotopy type theory is a recent approach to doing this very sort of thing for homotopy theory. Paths are not built as continuous maps from the unit interval of real numbers but instead are a primitive type in the theory.

Personally I would consider the term "synthetic homotopy theory" to perhaps be somewhat broader, encompassing the whole long line of attempts to preserve the content of homotopy theory while divorcing it from the classical description of a topological space.