RE: [HoTT] Is synthetic the right word?

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

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

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



________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of andré hirschowitz [mphm...@gmail.com]
Sent: Wednesday, June 15, 2016 2:26 PM
To: Homotopy Type Theory
Subject: [HoTT] Is synthetic the right word?

Hi,

Today, I have discovered that some (nice) members of this community do not like the word "synthetic" in the formula  "Synthetic Homotopy Theory" used in this group to name you know what.

My opinion is that people working is this area deserve an accepted name for this activity. So I consider that who finds this wording inadequate should either  argue HERE  and NOW, or shut down forever (on this precise topic!).

So?

andré


--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 3731 bytes --]