Is synthetic the right word?

Is synthetic the right word?

[andré hirschowitz]

[-- Attachment #1.1: Type: text/plain, Size: 452 bytes --]

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é


[-- Attachment #1.2: Type: text/html, Size: 508 bytes --]

RE: [HoTT] Is synthetic the right word?

[Joyal, André]

[-- 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 --]

Re: [HoTT] Is synthetic the right word?

[andré hirschowitz]

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

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

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

Re: [HoTT] Is synthetic the right word?

[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

Re: [HoTT] Is synthetic the right word?

[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


> On 16 Jun 2016, at 11:27, Andrej Bauer <andrej...@andrej.com> wrote:
> 
> 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
> 
> -- 
> 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

Re: [HoTT] Is synthetic the right word?

[Cale Gibbard]

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

Re: [HoTT] Is synthetic the right word?

[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

Re: [HoTT] Is synthetic the right word?

[andré hirschowitz]

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

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

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

Re: [HoTT] Is synthetic the right word?

[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

Re: [HoTT] Is synthetic the right word?

[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

On Thu, Jun 16, 2016 at 3:04 PM, andré hirschowitz <a...@unice.fr> wrote:
>
> 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
>
> --
> 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.

Re: [HoTT] Is synthetic the right word?

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

Re: [HoTT] Is synthetic the right word?

[Steve Awodey]

> On Jun 16, 2016, at 3:15 PM, Andrej Bauer <andrej...@andrej.com> wrote:
> 
> 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.

yes - this is of course correct.

Regards,
Steve

> 
> With kind regards,
> 
> Andrej
> 
> -- 
> 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.

Re: [HoTT] Is synthetic the right word?

[andré hirschowitz]

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

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

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

Re: [HoTT] Is synthetic the right word?

[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


On Thu, Jun 16, 2016 at 4:07 PM, andré hirschowitz <a...@unice.fr> wrote:
> 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
>
>
>
> --
> 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.

Re: [HoTT] Is synthetic the right word?

[Marc Bezem]

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

"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

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

Re: [HoTT] Is synthetic the right word?

[Eric Finster]

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

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


>
> On Thu, Jun 16, 2016 at 4:07 PM, andré hirschowitz <a...@unice.fr> wrote:
> > 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
> >
> >
> >
> > --
> > 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.
>
> --
> 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.
>

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

Re: [HoTT] Is synthetic the right word?

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

Re: [HoTT] Is synthetic the right word?

[Steve Awodey]

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

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

> On Jun 16, 2016, at 4:07 PM, andré hirschowitz <a...@unice.fr> wrote:
> 
> Hi!
> 
> 2016-06-16 15:15 GMT+02:00 Andrej Bauer <andrej...@andrej.com <mailto: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
>   
> 
> 
> 
> -- 
> 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 <https://groups.google.com/d/optout>.


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

RE: [HoTT] Is synthetic the right word?

[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é

RE: [HoTT] Is synthetic the right word?

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

On Thu, Jun 16, 2016 at 8:03 AM, Joyal, André <joyal...@uqam.ca> wrote:
> 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é
>
> --
> 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.

Re: [HoTT] Is synthetic the right word?

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

On 16 June 2016 at 12:28, Joyal, André <joyal...@uqam.ca> wrote:
> 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.
>
> On Thu, Jun 16, 2016 at 8:03 AM, Joyal, André <joyal...@uqam.ca> wrote:
>> 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é
>>
>> --
>> 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.
>
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] Is synthetic the right word?

[andré hirschowitz]

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

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

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

Re: [HoTT] Is synthetic the right word?

[Thierry Coquand]

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


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




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

Re: [HoTT] Is synthetic the right word?

[Eric Finster]

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

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

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

Re: [HoTT] Is synthetic the right word?

[Thierry Coquand]

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


 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

On 16 Jun 2016, at 19:51, Eric Finster <ericf...@gmail.com<mailto:ericf...@gmail.com>> wrote:

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


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

Re: [HoTT] Is synthetic the right word?

[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

Re: [HoTT] Is synthetic the right word?

[Eric Finster]

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

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

On Thu, Jun 16, 2016 at 8:18 PM Urs Schreiber <urs.sc...@googlemail.com>
wrote:

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

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

Re: [HoTT] Is synthetic the right word?

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

Re: [HoTT] Is synthetic the right word?

[Egbert Rijke]

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

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

On Thu, Jun 16, 2016 at 9:18 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
wrote:

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

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

RE: [HoTT] Is synthetic the right word?

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


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