Dear André H,

I was nice to meet you this afternoon and to be present at the Phd defense of Guillaume Brunerie.
I am very impressed by Brunerie's mastership in computing non-trivial homotopy groups of spheres
using exclusively the rules of homotopy type theory.

This afternoon, I have expressed my opposition to calling homotopy type theory
"Synthetic Homotopy Theory". You have expressed the desire
 to have a public discussion on this subject.

I will try to be clear and short.
The word "synthetic" suggests that a new kind of homotopy theory is born,
something that is changing the fabric of homotopy theory itself. I disagree.
This is not to diminish the importance of the work of Voevodsky, Shulman, Lumsdane, Licata,
Finster and Brunerie, on the contrary. Their work is original and absolutly beautiful.
 But the contribution of homotopy type theory to homotopy theory
is presently like the contribution of a stream to the flow of a river.
The stream may grow in time and eventually become the main stream, but we are not there yet!
Also, the water from the stream mixes very well with the water of the river.
It is building on classical concepts: fibrations, homotopy pullback,
homotopy pushout, homotopy fiber, suspension, loop space, connected space,
discrete space, classifying space, Freudenthal suspension theorem,
Blakers-Massey theorem, Eilenberg-MacLane spaces.
The "synthetic" label can make believe that the water
from the stream has a different nature. I find it divisive.
Homotopy type theory is the union of type theory with homotopy theory.
To divide is the last thing we need.

Best regards,
André J