Is synthetic the right word?

[andré hirschowitz]

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é

[Joyal, André]

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?

--
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.
For more options, visit https://groups.google.com/d/optout.

[andré hirschowitz]

Hi!

thanks for your quick reply.

2016-06-16 1:13 GMT+02:00 Joyal, André <joyal...@uqam.ca>:

The word "synthetic" suggests that a new kind of homotopy theory is born,

That is exactly the point. When speaking about Guillaume's work, you may want to stress that his result is completely new, because his sphere is not the classical sphere, and not even a shadow of the classical sphere in any reasonable sense. You could call it the synthetic sphere, or find a better wording. But a name is clearly needed for this new sphere and for this new homotopy theory.

andré H

[Andrej Bauer]

Various subjects have been called synthetic, and in every case I am
aware of the subject develops a branch of mathematics in (the internal
language of) a topos that is particularly suitable for the topic at
hand. Thus we have had Synthetic Differential Geometry, Synthetic
Domain Theory, Synthetic Topology and Synthetic Computability.

The word "synthetic" here refers to the fact that we create an
artificial, or synthetic, world of mathematics suitable for doing
whatever it is we are doing. For instance, the effective topos is
suitable for doing computability. If I am wrong about this particular
point, I would like to hear why Synthetic Differential Geometry was
originally so called.

The word "synthetic" does not refer to there being a completely new
thing that is different from what has been done so far. In the above
examples there is always a clear connection to the traditional ways,
with suitable transfer theorems guaranteeing that the synthetic world
is not just a hallucination.

In line with the established terminology, such as it may be, Synthetic
Homotopy Theory would be homotopy theory developed in (the internal
language of) a topos, or other suitable structure, that is
particularly suitable for doing homotopy theory. One may put a varying
amounts of emphasis on the internal language or the models, according
to taste. What I think we are lacking at the moment is a clear way of
transfering results in synthetic homotopy theory back to a traditional
setup. The explanation which says "interpretet in Kan simplicial sets
and apply the geometric realization" does not seem to be good enough,
or at least it should be made mathematically precise. Perhaps the we
should just forget about topology and use simplicial sets as the
natural traditional setup for doing homotopy theory?

We even have Synthetic Combinatorics, although its author prefers to
adopt terminology from biology and anthropology :-)

With kind regards,

Andrej

[Nicola Gambino]

Dear all,

I do not think that the word “synthetic” in these contexts is intended to mean “artificial”.

Instead, I think that it is used to denote the result of a synthesis. This is the same way in which “synthetic” is used in the expression “synthetic geometry”, as opposed to "analytic geometry”. In analytic geometry, we use coordinates to define points, lines, etc.., while in synthetic geometry these notions are taken as primitive. The two ways of doing geometry are related precisely.

There is a clear similarity with the situation in homotopy theory. Classical homotopy theory, in which topological spaces are defined via their points and open sets, is the analogue of analytic geometry. Homotopy theory done in model categories or in type theory is the analogue of synthetic geometry, and therefore it is not unreasonable to call it synthetic homotopy theory. An alternative would be to call it “axiomatic homotopy theory"

In either case, I think that adding “synthetic” or “axiomatic” to “homotopy theory” is not intended to suggest a different subject, but rather a different way of doing things.

Best wishes,
Nicola

> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

===
Dr Nicola Gambino
School of Mathematics
University of Leeds
E-mail: n.ga...@leeds.ac.uk

[Cale Gibbard]

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.

[Steve Awodey]

Dear Andre’ H.,

> On Jun 16, 2016, at 10:56 AM, andré hirschowitz <a...@unice.fr> wrote:
...

> When speaking about Guillaume's work, you may want to stress that his result is completely new, because his sphere is not the classical sphere, and not even a shadow of the classical sphere in any reasonable sense. You could call it the synthetic sphere, or find a better wording. But a name is clearly needed for this new sphere and for this new homotopy theory.

I don’t think it’s correct to say that the spheres, etc., of HoTT are new spheres. They are exactly the same spheres, only reasoned about in a new way. The proofs are different in some respects, but also the same in other respects. We are proving the same theorems, not new ones, using different methods of proof.

The interpretation of HoTT into axiomatic (categorical) homotopy theory, and then in turn into sSets, Top, etc., show that it is one subject — homotopy theory. But each degree of abstraction also expands the subject. In HoTT, one main difference is that the notion of a path, or a space, is taken as primive, rather than being analyzed into a sequence, or set, of points with some further structure. This difference is what we tried to describe with the term “synthetic”. Maybe we should put some more effort into explaining the choice of terminology, as the first round of papers start coming out for publication. That makes a discussion such as this one timely and useful — thanks for starting it!

Regards,

Steve

[andré hirschowitz]

2016-06-16 14:37 GMT+02:00 Steve Awodey <awo...@cmu.edu>:

They are exactly the same spheres

Hey!

It is extremely surprising to me that someone within this community believes this. My point was rather that you have to make clear, outside the community, that the theorems we talk about are new theorems, not just new (fancy?) ways to revisit the proof of old theorems. Now I understand that the job starts within the community.

I am afraid of the discussion which could follow if I try to argue that the synthetic sphere is definitely different of the classical one...

Sorry!

andré H

[Andrej Bauer]

On Thu, Jun 16, 2016 at 2:04 PM, andré hirschowitz <a...@unice.fr> wrote:
> I am afraid of the discussion which could follow if I try to argue that the
> synthetic sphere is definitely different of the classical one...

The HoTT objects, such as the circles and the spheres expressed as
HITs, may be interpreted in many different models, some of which will
give "old objects" and other "new ones". So at least at this level it
is a bit pointless to discuss things in absolute terms. The HoTT
proofs are *also* about the usual spheres.

With kind regards,

Andrej

[Bas Spitters]

Dear andré,

I am curious what you have to say. Does the case of the Blakers-Massey
theorem help?
https://ncatlab.org/nlab/show/Blakers-Massey+theorem#ReferencesInHoTT

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

Bas

[Urs Schreiber]

> 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.

[Steve Awodey]

yes - this is of course correct.

Regards,
Steve

>
> With kind regards,
>
> Andrej

[andré hirschowitz]

Hi!

2016-06-16 15:15 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:

So at least at this level it
is a bit pointless to discuss things in absolute terms. The HoTT
proofs are *also* about the usual spheres.

I disagree with this formulation. It is not at all pointless (with respect to positions, publications and the like) to make clear in which sense synthetic spheres strictly encompass classical ones (and potentially "non-euclidian" future ones).

And instead of stressing that these HoTT proofs are *also* about the usual spheres, we should rather stress that these HoTT proofs are *not at all only* about the usual spheres.

andré H

 

[Bas Spitters]

The Blakers-Massey theorem has *interesting* interpretations in other
oo-toposes.
Are you suggesting that the same may be true for the synthetic results
that have been proved about spheres?
The consensus seemed that be that that was not the case (yet?).

Bas

[Marc Bezem]

"And instead of stressing that these HoTT proofs are *also* about the usual spheres, we should rather stress that these HoTT proofs are *not at all only* about the usual spheres."

What are "usual spheres" given that any classical theory of real numbers also has non-standard models?

Marc

[Eric Finster]

The Blakers-Massey theorem has *interesting* interpretations in other
oo-toposes.

At least in the case which I know best, that of interpreting the theorem in the

presheaf topos [Fin_*, S] of functors on finite, pointed spaces to spaces, 

I don't think I would say that the interpretation is more interesting: it is just

interpreted pointwise.

It is rather the interaction of the theorem with another set of modalities in

[Fin_*, S] which I think is interesting, and gives some new results.

But since this topos lies outside of the realm in which we can interpret univalent

type theory right now, we still have to rely on the infty-categorified proof to

say that we indeed know the theorem holds. 

Eric

[Urs Schreiber]

> The Blakers-Massey theorem has *interesting* interpretations in other
> oo-toposes.
> Are you suggesting that the same may be true for the synthetic results
> that have been proved about spheres?
> The consensus seemed that be that that was not the case (yet?).

Indeed, for spheres the case is not so interesting..This is because,
at least in Grothendieck infinity-toposes H, then the fact that the
inverse image functor

H <--- S

from the base S (left adjoint to global section) preserves all
homotopy colimits and finite homotopy limits, means that the usual
spheres in H coincide with the usual spheres in S.

But synthetic homotopy theory is not only about spheres.

[Steve Awodey]

the spheres are not a very good example of the way in which synthetic objects may differ from classical ones, since they are homotopy colimits and therefore are preserved by inverse image functors. 

Steve

[Joyal, André]

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é

[Joyal, André]

Dear Michael,

Quillen homotopical algebra is very good for working in an infty-category
with finite limits and colimits, but it is not well adapted to exploit the specific
nature of an infty-topos. For this, we need a more powerful axiomatic system.
Axiomatic homotopy theory is what comes after Quillen homotopical algebra.
Axiomatic infty-topos theory could be the main branch.

One problem with the word "synthetic" is that it needs to be explained, and possibly justified.
Synthetic differential geometry is not popular among differential geometers.
The basic ideas are known and it is regarded with contempt. Sad.

Best regards,
André

________________________________________
From: Michael Shulman [shu...@sandiego.edu]
Sent: Thursday, June 16, 2016 11:17 AM
To: Joyal, André
Cc: Homotopy Type Theory
Subject: Re: [HoTT] Is synthetic the right word?

The problem is that by now, "axiomatic homotopy theory" has come to
essentially mean "Quillen model categories", so it gives no indication
of how "homotopy theory in type theory" differs from that. I still do
not see the problem with "synthetic". Many mathematicians are not
familiar with the word in this context, but that's not a problem; we
just explain what it means. Mathematicians are used to words having
precise meanings that have to be explained before they can be
understood.

[Cale Gibbard]

There is a certain irony in calling homotopy type theory "axiomatic",
in that one of the major directions that people hope to develop it is
to find nice axiom-free type theories (e.g. cubical type theory) in
which univalence can be a theorem.

But perhaps "axiomatic" is meant in a somewhat different sense there
-- one which can include the introduction and elimination rules of the
logic.

> You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/B1upabJFHRc/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[andré hirschowitz]

Hi!

2016-06-16 16:15 GMT+02:00 Bas Spitters <b.a.w.s...@gmail.com>:

Are you suggesting that the same may be true for the synthetic results
that have been proved about spheres?

No I do not want to suggest anything. I just consider that, as other explained very well in this conversation, the status of the synthetic sphere is completely different from the status of the (various?) classical spheres.

andré H

[Thierry Coquand]

But since this topos lies outside of the realm in which we can interpret univalent

type theory right now, we still have to rely on the infty-categorified proof to

say that we indeed know the theorem holds. 

 A small remark about this: at least we can interpret type theory with the univalence 

axiom in the (iterated) presheaf category

 [Fin_*, [C^op, Set]]

where C is the category of cubes we have considered for cubical type theory

(since we know how to interpret universes in presheaf categories and all the operations

relativize to presheafs; on the other hand, it is not clear yet how to relativize it for -sheaf- models

since it is less clear how universes should be interpreted).

We also should have a purely syntactical version, where judgements are indexed not only over a finite set

but over a pair of a finite set and a pointed finite set.

 Thierry

 

[Eric Finster]

Hi Thierry,

 

 A small remark about this: at least we can interpret type theory with the univalence 

axiom in the (iterated) presheaf category

 [Fin_*, [C^op, Set]]

where C is the category of cubes we have considered for cubical type theory

(since we know how to interpret universes in presheaf categories and all the operations

relativize to presheafs; on the other hand, it is not clear yet how to relativize it for -sheaf- models

since it is less clear how universes should be interpreted).

We also should have a purely syntactical version, where judgements are indexed not only over a finite set

but over a pair of a finite set and a pointed finite set.

Very interesting remark.

I'm not quite sure this quite corresponds to what I had in mind, since I was thinking of the 

infty-category of presheaves on the infty-category of finite pointed spaces.  (That is,

by Fin_* I mean finite *spaces*, not finite sets... sorry if my notation was bad)  With this in mind, I guess 

in the remark this would correspond to something like considering the "enriched" 

presheaves with some chosen model structure.  But I'm getting a bit out of my depth here

so maybe someone can chime in to help me out ...

So it looks to me like you are saying something like that the cubical model should tell

us how to interpret type theory in an infinity-topos of presheaves on an arbitrary 1-category?

Is this right, or am I misunderstanding? Or was Fin_* special for some reason (though, 

again, Fin_* for me was finite spaces, not finite sets ...)?  Can I replace Fin_* with D for any category D?

Fin_* certainly falls outside of the EI-category restriction, and I was not aware that

we knew how to lift that.  Does cubical type theory give a way or have I completely missed the point?  :p

Cheers,

Eric

[Thierry Coquand]

 Sorry for the misunderstanding!  Indeed, what I wanted to state was only 

something corresponding to

 -how to interpret type theory in an infinity-topos of presheaves on an arbitrary 1-category-

 and I misread what you wrote reading “finite set” instead of “finite space”...

    Thierry

[Urs Schreiber]

> was bad) With this in mind, I guess
> in the remark this would correspond to something like considering the
> "enriched"
> presheaves with some chosen model structure. But I'm getting a bit out of
> my depth here
> so maybe someone can chime in to help me out ...

The model structure that you are after here, for excisive functors,
modeled on the pointed topologically enriched category of finite
pointed CW-complex is discussed in

Michael Mandell, Peter May, Stefan Schwede, Brooke Shipley,
"Model categories of diagram spectra"
https://ncatlab.org/nlab/show/Model+categories+of+diagram+spectra

This is the topologically enriched version of Lydakis' simplicially
enriched model structure for excisive functors

https://ncatlab.org/nlab/show/model+structure+for+excisive+functors

[Eric Finster]

Hi,

Thierry:  Great!  That's really cool!  It hadn't occurred to me that cubicaltt had that kind of implication for the model theory.

Urs:  Thanks for the reference.  That's exactly the kind of thing I had in mind.

Cheers,

Eric

[Martin Escardo]

I sent this this morning only to Andrej this morning, which seems to
resonate with what people said later, in particular Nicola:

---- Thu, 16 Jun 2016 12:08:12 +0100
Andrej, you forgot to include synthetic geometry in your list (which
doesn't need a topos).

https://en.wikipedia.org/wiki/Synthetic_geometry
"Geometry, as presented by Euclid in the elements, is the quintessential
example of the use of the synthetic method."

We probably regard the synthetic circle as in some sense the same as the
analytic circle - although if our synthetic geometry doesn't have enough
axioms, it may be talking about the circle of another world.

And we make models of synthetic geometry in analytic geometry, but
synthetic geometry is intended to also stand on its own, without the
need of an analytical model.

Isn't the synthetic method (that of primitive notions "defined" by
axioms) everywhere? Even set theory is like that (we start with the
undefined primitive notions of set and membership, and use axioms to try
to capture some intuition we may have - we never actually say what a set
"really" is, other than giving intuitions such as "collections").

Similarly, when we do classical analysis, we work with a complete
Archimedian field, and not with the Dedekind or Cauchy reals (which we
can use as analytic models of the complete Archimedian field in set theory).
--/--

Now I add this: similarly, HoTT, UF or what-you-have, as some people
conceive, including myself, is intended to stand on its own, before we
consider any model, very much like Euclidean geometry.

What Andre Joyal disputes (and I did too in the previous thread) is not
the philosophy (or: better, point of view) but rather whether the words
which we use to advertise all of this have unintended connotations which
invoke the unintended meanings more than the intended one.

M.

[Egbert Rijke]

My experience, and I'm only speaking for myself, is that I have never really needed to use terminology such as "synthetic homotopy theory" when doing HoTT. The terminology "homotopy type theory", which to me refers to the synergy of homotopy theoretic and type theoretic methods and ideas, suffices for me.

In the HoTT book, the word "synthetic" was used either to contrast the synthetic method to the analytic method, or to emphasize the elementary nature of the proofs in Chapter 8. Phrases like "synthetic approach" have only appeared in the context of such an explanation, and not in isolation. Note that the phrase "synthetic homotopy theory" does not appear in the book.

With kind regards,

Egbert

[Joyal, André]

Dear Martin,

You wrote:

<What Andre Joyal disputes (and I did too in the previous thread) is not
the philosophy (or: better, point of view) but rather whether the words
which we use to advertise all of this have unintended connotations which
invoke the unintended meanings more than the intended one.>

That is exactly of my point.

Thank you.

Regards,
André

________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Martin Escardo [m.es...@cs.bham.ac.uk]
Sent: Thursday, June 16, 2016 3:18 PM
To: HomotopyT...@googlegroups.com

Subject: Re: [HoTT] Is synthetic the right word?

I sent this this morning only to Andrej this morning, which seems to

M.