Jacob Lurie and Higher Topos Theory?
592 views
Skip to first unread message
Mark Farrell
Feb 11, 2016, 11:55:31 AM2/11/16
to HoTT Cafe
Hi,
I've encountered and taken a brief, first look at Jacob Lurie's work on Higher Topos Theory.
http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
It appears as though his work is considerably aligned with the homotopy type theory programme and what is being studied in HoTT.
I'm surprised that he didn't, to the best of my knowledge, e.g. make an appearance during the special year, or e.g. isn't an invited speaker to this year's Workshop on Homotopy Type Theory.
Thoughts?
I suppose my question is: am I mistaken, and has anyone who works in HoTT spoken or collaborated with Jacob Lurie?
-Mark
I've encountered and taken a brief, first look at Jacob Lurie's work on Higher Topos Theory.
http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
It appears as though his work is considerably aligned with the homotopy type theory programme and what is being studied in HoTT.
I'm surprised that he didn't, to the best of my knowledge, e.g. make an appearance during the special year, or e.g. isn't an invited speaker to this year's Workshop on Homotopy Type Theory.
Thoughts?
I suppose my question is: am I mistaken, and has anyone who works in HoTT spoken or collaborated with Jacob Lurie?
-Mark
Michael Shulman
Feb 11, 2016, 11:59:16 AM2/11/16
to Mark Farrell, HoTT Cafe
I've talked with Jacob about HoTT, but he isn't very interested in it.
I gather that he prefers category-theoretic arguments to
type-theoretic ones.
> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
I gather that he prefers category-theoretic arguments to
type-theoretic ones.
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Bas Spitters
Feb 11, 2016, 12:06:39 PM2/11/16
to Michael Shulman, Mark Farrell, HoTT Cafe
This week we have a lecture room half full of higher category
theorists interested in HoTT.
https://www.mpim-bonn.mpg.de/node/6459
theorists interested in HoTT.
https://www.mpim-bonn.mpg.de/node/6459
Kevin Quirin
Feb 11, 2016, 11:07:37 PM2/11/16
to Mark Farrell, HoTT Cafe
Hi,
When asked, he just told « no comments ». He explained a bit more on Michael Harris’ blog : https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/
Urs Schreiber
Feb 12, 2016, 3:43:08 AM2/12/16
to Kevin Quirin, Mark Farrell, HoTT Cafe
It's an open secret that while HoTT has the clear potential to be
relevant for practicing homotopy theorists and higher topos
theorists, the field is not yet quite living up to it. There are a
tiny number of people, first and foremost Mike Shulman, who really
work on HoTT as a topic in higher topos theory. The progress
especially Mike has been making is impressive, but to homotopy
theorists who are not into type theory or foundations as such, the
development of HoTT is still at most at the verge of being
interesting.
Jacob Lurie is just the most prominent example, I could give you a
long list of names of top homotopy theory researchers who ought to be
interested in HoTT-as-it-could-once-be but are very dismissive about it
at the moment.
I think this ought to change, and it may change. But changing this
situation will require many more man-years of work on the aspects of
HoTT that are genuinely homotopy theoretic and higher topos theoretic.
Unfortunately, currently large parts of the field are actively pushing away from
this direction, wich does not help to improve the situation.
For instance all the work on initiality of models of type theory is
really something that belongs to traditional type theory and means
nothing to practicing mathematicians. One sees vivd evidence this week
where at MPI Bonn Vladimir is given a "marathon", as he announced it,
talk series on C-systems in the context of a prgram titled "Higher
structures in geometry and physics": it leaves most people except a
handful of accounting specialists utterly puzzled why they should care
about this, and nobody gets away with the impresion that there is
anything remotely to be gained here for topics that, say, a Jacob Lurie is
interested in.
Also the wealth of work on "cubical type theory" so far failed to
really connect to homotopy theory as such. The problem that it is
motivated by, to make univalence compute, is again something that
research homotopy theorists could not care less about; it's pushing
away from instead of towards the interest of people like Lurie.
In contrast, I think it is clear that what needs to be done next in
order to improve the impact of HoTT on research-level homotopy theory
is:
First and foremost, fill that darn remaining issue with the weak
Tarskian universes, such as to finally have as an official theorem
(instead of as something that Mike Shulman finds too obvious to
publish, while nobody else in the field understands) that HoTT has
interpretation in *every* infinity-topos as in Lurie's book, not just
in the (admittedly already imprressive) two or three classes of
infinite families of infinity-presheaf toposes (with strict universes)
that Mike has, thankfully, constructed. Mike explained this here
https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos
and if I were in charge of HoTT, I would drop everything else until
the statement on that webpage becomes an officially published article.
Second, really important would be to make progress on formalizing
stable homotopy theory, i.e. "spectrum types" or at least something in
this direction. Homotopy theory is so rich, that most computational
progress in practice is made by "linearizing" problems, in the sense
of Goodwillie calculus, hence by translating problems about homotopy
types into problems about stable homotopy types (spectra) as far as
possible.
For instance it's not too surprising that the HoTT community is
currently stuck with computing but the most evident homotopy groups of
spheres (another reason why any working homotopy theorist feels there
is nothing to be found here): this was precisely the state of the
field of homotopy theory, too, in the 50s, before stabilization and
spectral sequences came along.
Again, it's Mike Shulman who has started to push this topic from a
HoTT perspective
https://ncatlab.org/homotopytypetheory/show/spectral+sequences
but it would be immensely useful if more people in the field (anyone,
for that matter) picked this up and developed this further.
Spectral sequences is *the* tool in modern research level homotopy
theory (see the recent sensational proof of the Kervaire invariant one
problem), it's where all the meat it. But also, it's computational
very demanding. Therefore, potentially, there is a fantastic chance
here for any computer assisted homotopy theory, hence for HoTT. Once
you had a piece of Coq that would read in a tower of homotopy types
and which would then start crunching out the pages of its spectral
sequence, you would be assured that all those homotopy theorists who
previously had "no comment" to make on HoTT would start paying
attention.
In short, I think currently HoTT as a topic in homotopy theory has an
immense ratio of potential over realization. Anybody who cares about
this, and who might take a hint from reactions such as Jacob Lurie's,
should think about investing more energy into research that actually
goes in this direction. Go an contact Mike Shulman, if you are not
sure which precise research questions to tackle. Read all his
articles, to see what the state of the field of HoTT as a topic in
homotopy theory is. Then work on this. I am optimistic that with
effort spend in this direction, eventually people like Jacob Lurie
will tak notice.
Best wishes,
urs
>> <mailto:hott-cafe+...@googlegroups.com>.
relevant for practicing homotopy theorists and higher topos
theorists, the field is not yet quite living up to it. There are a
tiny number of people, first and foremost Mike Shulman, who really
work on HoTT as a topic in higher topos theory. The progress
especially Mike has been making is impressive, but to homotopy
theorists who are not into type theory or foundations as such, the
development of HoTT is still at most at the verge of being
interesting.
Jacob Lurie is just the most prominent example, I could give you a
long list of names of top homotopy theory researchers who ought to be
interested in HoTT-as-it-could-once-be but are very dismissive about it
at the moment.
I think this ought to change, and it may change. But changing this
situation will require many more man-years of work on the aspects of
HoTT that are genuinely homotopy theoretic and higher topos theoretic.
Unfortunately, currently large parts of the field are actively pushing away from
this direction, wich does not help to improve the situation.
For instance all the work on initiality of models of type theory is
really something that belongs to traditional type theory and means
nothing to practicing mathematicians. One sees vivd evidence this week
where at MPI Bonn Vladimir is given a "marathon", as he announced it,
talk series on C-systems in the context of a prgram titled "Higher
structures in geometry and physics": it leaves most people except a
handful of accounting specialists utterly puzzled why they should care
about this, and nobody gets away with the impresion that there is
anything remotely to be gained here for topics that, say, a Jacob Lurie is
interested in.
Also the wealth of work on "cubical type theory" so far failed to
really connect to homotopy theory as such. The problem that it is
motivated by, to make univalence compute, is again something that
research homotopy theorists could not care less about; it's pushing
away from instead of towards the interest of people like Lurie.
In contrast, I think it is clear that what needs to be done next in
order to improve the impact of HoTT on research-level homotopy theory
is:
First and foremost, fill that darn remaining issue with the weak
Tarskian universes, such as to finally have as an official theorem
(instead of as something that Mike Shulman finds too obvious to
publish, while nobody else in the field understands) that HoTT has
interpretation in *every* infinity-topos as in Lurie's book, not just
in the (admittedly already imprressive) two or three classes of
infinite families of infinity-presheaf toposes (with strict universes)
that Mike has, thankfully, constructed. Mike explained this here
https://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+(infinity,1)-topos
and if I were in charge of HoTT, I would drop everything else until
the statement on that webpage becomes an officially published article.
Second, really important would be to make progress on formalizing
stable homotopy theory, i.e. "spectrum types" or at least something in
this direction. Homotopy theory is so rich, that most computational
progress in practice is made by "linearizing" problems, in the sense
of Goodwillie calculus, hence by translating problems about homotopy
types into problems about stable homotopy types (spectra) as far as
possible.
For instance it's not too surprising that the HoTT community is
currently stuck with computing but the most evident homotopy groups of
spheres (another reason why any working homotopy theorist feels there
is nothing to be found here): this was precisely the state of the
field of homotopy theory, too, in the 50s, before stabilization and
spectral sequences came along.
Again, it's Mike Shulman who has started to push this topic from a
HoTT perspective
https://ncatlab.org/homotopytypetheory/show/spectral+sequences
but it would be immensely useful if more people in the field (anyone,
for that matter) picked this up and developed this further.
Spectral sequences is *the* tool in modern research level homotopy
theory (see the recent sensational proof of the Kervaire invariant one
problem), it's where all the meat it. But also, it's computational
very demanding. Therefore, potentially, there is a fantastic chance
here for any computer assisted homotopy theory, hence for HoTT. Once
you had a piece of Coq that would read in a tower of homotopy types
and which would then start crunching out the pages of its spectral
sequence, you would be assured that all those homotopy theorists who
previously had "no comment" to make on HoTT would start paying
attention.
In short, I think currently HoTT as a topic in homotopy theory has an
immense ratio of potential over realization. Anybody who cares about
this, and who might take a hint from reactions such as Jacob Lurie's,
should think about investing more energy into research that actually
goes in this direction. Go an contact Mike Shulman, if you are not
sure which precise research questions to tackle. Read all his
articles, to see what the state of the field of HoTT as a topic in
homotopy theory is. Then work on this. I am optimistic that with
effort spend in this direction, eventually people like Jacob Lurie
will tak notice.
Best wishes,
urs
>> For more options, visit https://groups.google.com/d/optout
>> <https://groups.google.com/d/optout>.
Michael Shulman
Feb 12, 2016, 4:39:04 PM2/12/16
to Urs Schreiber, Kevin Quirin, Mark Farrell, HoTT Cafe
Since my name got dropped a lot there, let me briefly summarize my own
point of view.
It's too bad that homotopy theorists and higher category theorists are
dismissive of HoTT. On the other hand, trying too hard to sell it to
them right now is part of what produces this dismissive attitude,
since when they ask "what will it do for me?" the answer has to be
"right now, not much". I think we're actually fairly far from the
verge of being *useful* to such people.
Part of making such a dream come true is working on the specific
higher-categorical aspects of HoTT. But work on the foundations of
HoTT is also an essential part of it. HoTT as a subject is young and
its foundations are in flux, and that shouldn't be ignored. In
particular, the initiality of models of type theory is *essential* for
any application of HoTT to higher category theory to be mathematically
rigorous; so it is absolutely something that people should be working
on EVEN IF the only thing one cared about were applications to
homotopy theory. (Which is, of course, a different thing from
thinking that homotopy theorists would be *interested* in the details
of this work. Obviously they will not be and we should not bother
them with it; to them it should be be a black box, but someone needs
to put the internals of that box in order.) Having a good
computational version of HoTT also has the potential to improve the
subject a lot, including its potential applications to homotopy theory
and category theory.
As for weak Tarski universes, in addition to not feeling that they
merit publication on their own, one reason I have not emphasized them
too much is that I am still hoping we will be able to build
categorical models of strong universes, and all actual work in HoTT to
date uses strong universes -- for the good reason that weak Tarski
universes are pretty annoying. Instead of impatiently grabbing at the
first possible way that HoTT might be applied to higher category
theory, it's worth thinking seriously about the foundations of the
subject before trying to sell it, especially since the currently
available applications are not all that "killer" yet.
Yes, we should definitely work on spectra and spectral sequences.
There is a group working on formalizing them right now, in fact. But
foundational work is also important. And patience.
Mike
point of view.
It's too bad that homotopy theorists and higher category theorists are
dismissive of HoTT. On the other hand, trying too hard to sell it to
them right now is part of what produces this dismissive attitude,
since when they ask "what will it do for me?" the answer has to be
"right now, not much". I think we're actually fairly far from the
verge of being *useful* to such people.
Part of making such a dream come true is working on the specific
higher-categorical aspects of HoTT. But work on the foundations of
HoTT is also an essential part of it. HoTT as a subject is young and
its foundations are in flux, and that shouldn't be ignored. In
particular, the initiality of models of type theory is *essential* for
any application of HoTT to higher category theory to be mathematically
rigorous; so it is absolutely something that people should be working
on EVEN IF the only thing one cared about were applications to
homotopy theory. (Which is, of course, a different thing from
thinking that homotopy theorists would be *interested* in the details
of this work. Obviously they will not be and we should not bother
them with it; to them it should be be a black box, but someone needs
to put the internals of that box in order.) Having a good
computational version of HoTT also has the potential to improve the
subject a lot, including its potential applications to homotopy theory
and category theory.
As for weak Tarski universes, in addition to not feeling that they
merit publication on their own, one reason I have not emphasized them
too much is that I am still hoping we will be able to build
categorical models of strong universes, and all actual work in HoTT to
date uses strong universes -- for the good reason that weak Tarski
universes are pretty annoying. Instead of impatiently grabbing at the
first possible way that HoTT might be applied to higher category
theory, it's worth thinking seriously about the foundations of the
subject before trying to sell it, especially since the currently
available applications are not all that "killer" yet.
Yes, we should definitely work on spectra and spectral sequences.
There is a group working on formalizing them right now, in fact. But
foundational work is also important. And patience.
Mike
Andrej Bauer
Feb 13, 2016, 12:57:55 PM2/13/16
to HoTT Cafe
If I understood correctly some of the remarks that Eric Finster made
yesterday at the discssion here in Bonn, the higher-structures people
would already beenfit from simply having a slightly more precise way
of talking to each other, even if this new way of talking isn't 100%
supported by a rock-solid foundation.
So perhaps a good start would be to write an *informal* paper which
describes what *informal* habits one has to change and what new ones
to adopt in order to be able to speak a little better about higher
structures. Would that be a worthwhile thing to do? We don't need
univalence and whatnot, just the basic idea that type theory is a
proof-relevant formalism and that everything is "automaically
continuous" so that one can explain why the definition of
contractibility is contractibility and not path-connectedness.
With kind regards,
Andrej
yesterday at the discssion here in Bonn, the higher-structures people
would already beenfit from simply having a slightly more precise way
of talking to each other, even if this new way of talking isn't 100%
supported by a rock-solid foundation.
So perhaps a good start would be to write an *informal* paper which
describes what *informal* habits one has to change and what new ones
to adopt in order to be able to speak a little better about higher
structures. Would that be a worthwhile thing to do? We don't need
univalence and whatnot, just the basic idea that type theory is a
proof-relevant formalism and that everything is "automaically
continuous" so that one can explain why the definition of
contractibility is contractibility and not path-connectedness.
With kind regards,
Andrej
Bas Spitters
Feb 14, 2016, 4:15:08 AM2/14/16
to Andrej Bauer, HoTT Cafe
This was one of the fields that was mentioned:
https://ncatlab.org/nlab/show/geometric+representation+theory
https://ncatlab.org/nlab/show/geometric+representation+theory
Urs Schreiber
Mar 8, 2016, 8:28:21 AM3/8/16
to HoTT Cafe
On Sunday, February 14, 2016 at 10:15:08 AM UTC+1, Bas Spitters wrote:
> This was one of the fields that was mentioned:
> https://ncatlab.org/nlab/show/geometric+representation+theory
By the way, if by "geometric representation theory" you mean constructions in representation theory involving *D-modules* [1], then it is precisely the axioms of "differentially cohesive homotopy-type theory" [2] that capture this synthetically.
Namely the modal operator "infinitesimal shape" Im [3] is such that putting an Im-modal type Im(X) into context, then the resulting homotopy theory has the interpretation of being that of partial differential equations with variables ranging in X. Restricting to the linear types here, these are, synthetically, the D-modules over X.
Moreover, generally representation theory of a group G is homotopy theory in the context of BG, see the table here: [4]. Combining this, one gets a synthetic formulation of representation theory and D-modules, hence a good deal of geometric representation theory.
Exposition and survey of what I just said is in [5], and from a broader perspective of variational calculus and local field theory in [6].
These references are not phrased in formal HoTT, but in the pseudocode formerly known as mathematics. However, the constructions they survey are such that they should lend themselves to full formalization. In fact [5] is meant and is phrased as an exercise sheet for ambitious young synthetic homotopy type theorists: the exercise is to fully formalize the constructions and theorems discussed there. They are selected such as to have a large ratio of research interest over expected difficulty. One student of mine is working on this, but there is material enough for plenty more activity.
[1] https://ncatlab.org/nlab/show/D-module
[2] https://ncatlab.org/nlab/show/differential+cohesion
[3] https://ncatlab.org/nlab/show/infinitesimal+shape+modality
[4] https://ncatlab.org/nlab/show/representation+theory
[5] https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory
[6] https://ncatlab.org/schreiber/show/Higher+Prequantum+Geometry
Namely the modal operator "infinitesimal shape" Im [3] is such that putting an Im-modal type Im(X) into context, then the resulting homotopy theory has the interpretation of being that of partial differential equations with variables ranging in X. Restricting to the linear types here, these are, synthetically, the D-modules over X.
Moreover, generally representation theory of a group G is homotopy theory in the context of BG, see the table here: [4]. Combining this, one gets a synthetic formulation of representation theory and D-modules, hence a good deal of geometric representation theory.
Exposition and survey of what I just said is in [5], and from a broader perspective of variational calculus and local field theory in [6].
These references are not phrased in formal HoTT, but in the pseudocode formerly known as mathematics. However, the constructions they survey are such that they should lend themselves to full formalization. In fact [5] is meant and is phrased as an exercise sheet for ambitious young synthetic homotopy type theorists: the exercise is to fully formalize the constructions and theorems discussed there. They are selected such as to have a large ratio of research interest over expected difficulty. One student of mine is working on this, but there is material enough for plenty more activity.
[1] https://ncatlab.org/nlab/show/D-module
[2] https://ncatlab.org/nlab/show/differential+cohesion
[3] https://ncatlab.org/nlab/show/infinitesimal+shape+modality
[4] https://ncatlab.org/nlab/show/representation+theory
[5] https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory
[6] https://ncatlab.org/schreiber/show/Higher+Prequantum+Geometry
Bas Spitters
Mar 8, 2016, 8:38:07 AM3/8/16
to Urs Schreiber, Richard Garner, HoTT Cafe
Richard Garner was the one who mentioned
https://ncatlab.org/nlab/show/geometric+representation+theory
in Bonn, I am CC-ing him in case he wants to comment.
Bas
https://ncatlab.org/nlab/show/geometric+representation+theory
in Bonn, I am CC-ing him in case he wants to comment.
Bas
Reply all
Reply to author
Forward
0 new messages