RE: [HoTT] Is synthetic the right word?

["Joyal, André" <"joyal..."@uqam.ca>]

Thank you all,

I hope you will forgive me if I try to answer you all in one message.

I understand the opposition between "synthetic" and "analytic" and I truly believe 
that univalent type theory is bringing something new to homotopy theory. 
But my concern is more sociological than philosophical. 
Homotopy theory is a well established field of mathematics
and homotopy theorists are not stupid (no offense).

 J.H.C. Whitehead wrote in 1950:

"The ultimate aim of algebraic homotopy is to construct a purely algebraic theory, 
which is equivalent to homotopy theory in the same sort of way that ‘analytic’ is 
equivalent to ‘pure’ projective geometry".

A giant step in that direction was the creation of homotopical algebra
by Daniel Quillen (1967).

The notion of Quillen model category enjoys many of the virtues attributed to homotopy type theory.
Also the notion of Brown fibration category.
It happens that the syntactic category of homotopy type theory
is a Brown fibration category (by a result of Avigad, Kapulkin and Lumsdaine)
The notion of path object can be defined in any Brown fibration category.
The fact that spheres can constructed in homotopy type theory
(with higher inductive types) is not surprising, once the connection 
between Martin-Lof type theory and homotopy theory is understood
(thanks to the work of Awodey and Warren). 

This been said, homotopy type theory offer a formal description of
important constructions in the homotopy theory of spaces and stacks.
The analogy with the theory of elementary toposes is striking,
since the latter is a categorical description of important constructions in the theory of sets and sheaves.
The fact that formal logic can contribute to homotopy theory came as a surprise.
But is often the way mathematics advance.

Homotopy type theory is presently in its infancy.
I hope it will keep growing but it is hard to predict the future directions.
It should remain axiomatic.
Nicola Gambino has proposed "Axiomatic homotopy theory".
It is the line of a tradition and it leaves the future open.

Best regards,
André