You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I gave a talk on Saturday at a conference -- The Future of the Humanities: Reflective Practices in the Age of AI. Rather ironic to have been asked to speak at the event when my Philosophy department at Kent is to close this summer.
My slides are here. I was speaking about ACT and AI/computer science, and raising questions about philosophical precursors. Take for instance the recent Bonchi et al. article Diagrammatic Algebra of First Order Logic, further uptake of Charles Peirce's existential graphs. Seeing that the original philosophical ideas generally come embedded within a whole system, I was wondering about the profit for the current user of such ideas in delving into their larger context.
I'm taking this theme a little further forward in a final department talk next Tuesday (11 June). You can watch online from 15.30 (UK time, so 14.30 GMT) on Teams (link).
This issue has come even closer to the front of my mind after acting as 'opponent' at @Nathan Haydon 's PhD defence last week, and some conversations I've had with a couple of Symbolica people.
There's a way to glimpse things where ACT allows us to extract something quite coherent from a multitude of philosophical voices.
By the way, Nathan passed!
Springer has just brought out a volume, Rethinking Thomas Kuhn’s Legacy, containing a chapter by me. It's titled Thomas Kuhn, Modern Mathematics and the Dynamics of Reason and probes the question of whether modern mathematics can be said to undergo revolutions, using higher category theory to illustrate. A very late draft is here.
Nice! I like this jab:
We would have been better prepared for this eventuality had it been expected of those philosophers tasked with understanding issues arising from mathematics that they attend to currents within active mathematical research...
If someone asked me whether modern mathematics can be said to undergo revolutions, I'd ask them about mathematics in general. Has it ever undergone revolutions? I can imagine someone saying "no", though I'd say "yes". If someone says mathematics has undergone revolutions in the past but is not doing so today, I can imagine two reasons:
1) mathematics is so well established that it's impossible to stage a revolution anymore
2) mathematics is sufficiently well established that it's harder, though not impossible to stage a revolution, and we happen to be living in a period between revolutions.
Anyway, your paper is a lot more well thought-out than this initial reaction! I just couldn't help it.
John Baez said:
Nice! I like this jab
Seems I can't help myself adding such jabs. I'm not sure I ever got over hearing in one of my first philosophy classes the lecturer replying to a question about category theory that it was far too difficult for us to bother with. And so it has largely continued for over 30 years.
Maybe by now you should ask if it's possible for old mathematics to have once had revolutions.
Mac Lane, Eilenberg and Grothendieck are all dead; maybe it's safe for philosophers to start paying attention to them.
I'm giving a couple of talks next week in Oxford:
Charles Peirce, Inference, and Category Theory
The American philosopher Charles Saunders Peirce (1839-1914) had much to say about the nature of intellectual enquiry. In the realm of deductive logic, category theorists have made important use of his string-diagrammatic logical calculus. But Peirce's interests in inference extended beyond deduction to induction and abduction. In this talk I shall be exploring the thesis that we can understand this triple in terms of the category-theoretic notions of composition, extension and lift. We will also touch on his broader semiotics and his account of concept formation.
( I'll make the slides available. It's very much an exploration, and there are plenty of paths to pursue, so I'd love to hear any comments people have.)
Linear homotopy type theory: its origins and potential uses
Linear homotopy type theory has arisen out of the Sati-Schreiber program in theoretic physics, which seeks to formulate M-theory, the hypothetical theory of which 11-dimensional supergravity and the five string theories are all special limiting cases. But there are plenty of points of considerable interest arising from it for researchers working in other fields: mathematics, quantum computing, data analysis, and even philosophy. Indeed, linear HoTT has implications for the philosophy of quantum mechanics, by providing a logical calculus which unites the Everettian many-worlds interpretation with the Copenhagen interpretation.
In this talk, I shall be offering personal reflections on why people might be interested in this new type theory.
I'll be in Oxford from Wednesday 19th. If anyone there would like to chat, then DM me.
David Corfield said:
Indeed, linear HoTT has implications for the philosophy of quantum mechanics, by providing a logical calculus which unites the Everettian many-worlds interpretation with the Copenhagen interpretation.
As someone interested in quantum foundations, I'm very curious about how this works! For instance, how can the single-world (and sometimes non-unitary) nature of the Copenhagen interpretation be "united" with the distinct many-world (and purely unitary) nature of the Everettian interpretation?
The linear modal calculus shows as equal two processes that lend themselves to the different interpretations. It's in several of the papers of this program, but one place is The Quantum Monadology, for instance from p. 7:
I doubt this will satisfy those who seek a single correct interpretation of what's 'really' going on.
I didn't mention that the OASIS talk is available online
Friday 21, 14.00
https://cs-ox-ac-uk.zoom.us/j/99562853810?pwd=VmJFUlhNbVJwOUpjTE5hUk9LUkMvUT09
Meeting ID: 995 6285 3810
Passcode: 983333
The thing I'm left wondering from that excursion is whether linear HoTT will provide a general way to deal with dependent substructural type theory. It rests on what gets called the 'miracle' that the tangent -category to is still an -topos. So one start out with HoTT and adjoin various devices, a self-adjoint modality , , .
And this linear HoTT can do good work even in down-to-earth finite-dimensional Hilbert space situations (cf. the latest exposition). But then where are the limits of its range of application?
What is the tangent category to ? In other word, does it have some snappy alternative description?
Parameterized spectra. Fiberwise stabilization of the codomain fibration.
Joyal (who else?) noticed it early.
Nice! I'm amazed, actually, that I understand your answer and it makes perfect sense.
Something I'm trying to figure out is how to relate this to @Mike Shulman telling us in his Framed bicategories and monoidal fibrations that parameterized spectra are best treated by double categories/framed bicategories.
It looks like for the uses of linear HoTT in physics one doesn't need the bimodule-like flavour of parameterization by an and a , but was that part of the May and Sigurdsson story that Mike was responding to?
I associate the term "parametrized spectrum" with Peter May, simply because he was the first high-powered homotopy theorist I hung out with for a long time, and this was the sort of concept that scared me, which was familiar.
I think there are more reasons for the association than that -- Peter and Johann Sigurdsson wrote a long book about parametrized spectra that I believe was the first modern treatment, and introduced a bunch of new important ideas and applications.
I wouldn't say that they are best treated by double categories, though. I would say that they are naturally an indexed/fibered monoidal category, and that it's a general fact about indexed monoidal categories that there is an associated double category that's useful for many things.
I wasn't knowledgeable enough to realize Peter May did crucial work on parametrized spectra. I just know that when I visited Chicago he would say things like "parametrized spectra" a lot, leaving Tom Leinster, Eugenia Cheng and I somewhat mystified.
But anyway, I know now - thanks!
Mike Shulman said:
I wouldn't say that they are best treated by double categories, though
Ah, OK. So maybe in these classically-controlled quantum physics situations the issue is that for any particular measurement there is just a type of outcomes and we don't need to partition this type to see things bi-parametrically.
John Baez said:
I wasn't knowledgeable enough to realize Peter May did crucial work on parametrized spectra.
He co-wrote a 441-page book on [[Parametrized Homotopy Theory]].
John Baez said:
leaving Tom Leinster, Eugenia Cheng and I somewhat mystified.
After your grammatical correction to me, perhaps I should say something about pronoun declension.
In these slides, Peter May (on slide 19) turns bimodule-wards when he comes to [[Spanier-Whitehead duality]] as treated by Costenoble and Waner:
image.png
image.png
leaving Tom Leinster, Eugenia Cheng and I somewhat mystified.
Yuck!
Well, I have no memory of that.
Here I'm asking @Mike Shulman about dependent linear type theory in the context of a post where he's telling us about Costenoble-Waner duality:
image.png
His reply ends:
However, to deal with linearity, we need a bicategory whose objects are categories. To formulate that in a similar way to the above, we’d need the “nonlinear types” to be categories, so that their type theory would be some sort of directed type theory. But without a general context in which to perform the derivator-to-bicategory construction, it’s not obvious to me exactly what this directed type theory should look like, or how it should interact with the dependent linear types.
Sounds like we need directed linear HoTT.
David Corfield said:
( I'll make the slides available. It's very much an exploration, and there are plenty of paths to pursue, so I'd love to hear any comments people have.)
What I have so far is here.
Mike Shulman said:
...it's a general fact about indexed monoidal categories that there is an associated double category that's useful for many things.
I didn't know this, but it seems intriguing. Where to look for more information about this?
Framed bicategories and monoidal fibrations, which David mentioned up above.
David Corfield said:
The thing I'm left wondering from that excursion is whether linear HoTT will provide a general way to deal with dependent substructural type theory. It rests on what gets called the 'miracle' that the tangent -category to is still an -topos. So one start out with HoTT and adjoin various devices, a self-adjoint modality , , .
Regarding this procedure for obtaining the theory of the tangent topos from the theory of some topos by adjoining new symbols, is that explicitly described somewhere? Here I really mean a Grothendieck topos seen as an elementary topos (not as a topos classifying some geometric theory).
It needs to be an -topos, some info here.
So then we're dealing with infinitesimal cohesion. Does that help?
David Corfield said:
It needs to be an -topos, some info here.
So then we're dealing with infinitesimal cohesion. Does that help?
Ah, yes. By topos I always mean -topos.
Perhaps I'm misunderstanding the initial comment of what one gets after adjoining those "various devices" you'd mentioned. Were you maybe describing instead how to get linear HoTT from HoTT?
I initially was thinking you were claiming something like: if we start with an extension of HoTT such that its category of contexts presents a certain specific topos, then there's some explicit manual procedure (by throwing new types and constructors) that extends the theory to another one such that the category of contexts of the latter presents the tangent topos and the inclusion of theories presents the inverse image. Was that the claim?
Fernando Yamauti said:
Perhaps I'm misunderstanding the initial comment of what one gets after adjoining those "various devices" you'd mentioned. Were you maybe describing instead how to get linear HoTT from HoTT?
That's all I'm saying. Sorry if it was misleading.
I'm joining Riley in being pleased that we can build on HoTT:
can you point me to this paper?
This is Mitchell Riley's thesis.
David Corfield said:
That's all I'm saying. Sorry if it was misleading.
I'm joining Riley in being pleased that we can build on HoTT:
Ah! Ok. That explains my confusion. You are talking about a newer definition of linear HoTT I was not aware of (where the base cat is a topos instead of a more general monoidal cat). So, in this case, models of linear HoTT are also models of HoTT, right? If so (up to local presentability), models extending the theory of some topos seems to be necessarily of the form for some locus.
That still makes me wonder whether the tangent topos is special among the models of linear HoTT. Perhaps it's the smallest model containing the topos and also something linear? But I don't know if this linear part is always fiberwise stable (?).
David Corfield said:
This is Mitchell Riley's thesis.
thank you!
Fernando Yamauti said:
So, in this case, models of linear HoTT are also models of HoTT, right?
Right.
Fernando Yamauti said:
That still makes me wonder whether the tangent topos is special among the models of linear HoTT. Perhaps it's the smallest model containing the topos and also something linear? But I don't know if this linear part is always fiberwise stable (?).
I don't know if people have thought about these questions. To give some context to the concept of 'infinitesimal cohesion', in the 1-category world it appears in the work of Lawvere on [[quality types]].
After the tangent topos, there's are [[jet toposes]] (so tangent = 1-jet). They interpolate between a topos and its arrow category, and so are relevant for [[twisted cohomology]]:
Looking back at this nForum discussion, it looks like we do have other candidates for genuine models of linear HoTT which aren't tangent toposes. There's what's being called there and .
Also worth noting that one may form the -linear tangent topos for any -ring spectrum, .
David Corfield said:
After the tangent topos, there's are [[jet toposes]] (so tangent = 1-jet). They interpolate between a topos and its arrow category, and so are relevant for [[twisted cohomology]]:
Looking back at this nForum discussion, it looks like we do have other candidates for genuine models of linear HoTT which aren't tangent toposes. There's what's being called there and .
Hmm... So up to presentability issues, it seems models of linear HoTT should be exactly for some locus (in the sense of Joyal) with a object, right?
Btw, why should the jet topoi interpolate between the base topos and the Sierspinski one (everything over the same base)? The nForum discussion seems to claim only the existence of an essential geometric morphism from the Sierpinski topos to the topos classifying pointed objects (the direct image is the left Kan extension of the restriction of functors). To show such an interpolation one would need instead a geometric morphism in the opposite direction that also factors through every jet topos.
David Corfield said:
Also worth noting that one may form the -linear tangent topos for any -ring spectrum, .
I might be wrong, but I don't think that is always a topos, so it can't be a model of linear HoTT. But perhaps you have something else in mind...
Fernando Yamauti said:
I might be wrong, but I don't think that is always a topos, so it can't be a model of linear HoTT. But perhaps you have something else in mind...
I was taking this from here:
image.png
Do you think it's wrong?
(I'll think about your earlier question.)
David Corfield said:
Fernando Yamauti said:
I might be wrong, but I don't think that is always a topos, so it can't be a model of linear HoTT. But perhaps you have something else in mind...
I was taking this from here:
image.pngDo you think it's wrong?
(I'll think about your earlier question.)
No. You're right. My bad. I thought you were talking about the tangent category of the cat of -algebras (which is usually defined as the fiberwise stabilisation of the codomain fibration).
The one you shared in the above image is indeed a topos and that follows from the main thm in Hoyois' paper proving the conjecture of Joyal.
Fernando Yamauti said:
Btw, why should the jet topoi interpolate between the base topos and the Sierspinski one (everything over the same base)?
Let's see what we have. So have the jet toposes defined as:
where the tangent topos is the -jet. And we have from the [[nLab]]:
For
for the full sub--category of the -functor -category on those -functors which are -excisive.
The inclusion is of a left exact reflective sub--category, hence the inclusion functor has a left adjoint
which moreover is left exact.
As ranges, the tower of -excisive approximations of an -functor forms a tower analogous to the the Taylor series of a smooth function. This is called the Goodwillie-Taylor tower.
We're approximating functors in , which is being denoted , by -excisive approximations.
So it's not interpolation to the Sierpinski topos, but to .
There's a coreflective inclusion of the Sierpinski topos into the pointed object classifying topos.
But we then have Urs saying:
Now the Sierpinski topos canonically maps to , but not fully faithfully so. Hence the Goodwillie tower construction does not in any evident way just restrict to the Sierpinski topos. But the "sectioned" Sierpinski topos fixes that, the -presheaves on the generic section diagram , which are bundles in that in addition are equipped with a section. This does have a fully faithful embedding into . And since does have a 0-object, is infinitesimally cohesive over .
David Corfield said:
So it's not interpolation to the Sierpinski topos, but to .
There's a coreflective inclusion of the Sierpinski topos into the pointed object classifying topos.
Thanks for the reply. But I'm not seeing anything new from what was already in the nForum discussion. Perhaps I'm missing something trivial.
For me, when you said "interpolation", I was expecting something like
or
where we also have the other -th jet topoi in between (the whole tower).
From what you said, at best, we only get an adjunction
which can possibly be a geometric morphism (is the left adjoint trivially left exact?). If that's the case, we still need a factorization through all the jet topoi. But, even for we only get a factorisation in the "wrong direction"
Fernando Yamauti said:
For me, when you said "interpolation", I was expecting...
I'm really no kind of expert on this material. I was trying to report what I'd understood from discussions years ago. If there's a mistake or something misleading on an nLab page, let's take that to the nForum.
Are you objecting to the wording (or my paraphrase of the wording) of the first section of [[twisted cohomology]]?
In this sense the tangent -topos is the lowest order linear approximation to the codomain fibration
If the wording on the nLab could be clearer, you could post on this nForum thread.
David Corfield said:
Are you objecting to the wording (or my paraphrase of the wording) of the first section of [[twisted cohomology]]?
In this sense the tangent -topos is the lowest order linear approximation to the codomain fibration
If the wording on the nLab could be clearer, you could post on this nForum thread.
No. That first section of "twisted coh" is fine. What's bothering me is the word "interpolate" in
David Corfield said:
[...]They interpolate between a topos and its arrow category, and so are relevant for [[twisted cohomology]]:
That looks like something like
Btw, the rightmost object should be in my previous reply (a typo, sorry) and not .
If that doesn't clarify my objection/misunderstanding, I will post on the nForum some days later (I can't use my computer for a couple of days and typing math on the cellphone is extremely annoying).
Perhaps you meant to say something like: the Sierpinski topos interpolate between the jet topos and the topos. That means
If so, I do agree. That's completely correct.
What is confusing me is Urs question on what should be . So I was expecting your claim to be that there was some topos bounding this limit from below and that the topos of sections or the Sierpinski one would do the job.
OK, that looks right.
And these other toposes? So is just the functor category from which the -jets carve out the -excisive functors.
Then what role is playing?
David Corfield said:
OK, that looks right.
What looks right? I'm confused...
Fernando Yamauti said:
What looks right? I'm confused...
Sorry, I meant your:
.
Ah! Ok. So by interpolation you meant
and
, right?
If so, that clarifies the confusion. But when someone say something interpolate between two things, I would usually assume this something is located between (as opposed to the extremities).
David Corfield said:
- Thurs 20, 14.00, Topos Institute (recorded but not live)
Charles Peirce, Inference, and Category Theory
Slides and recording are available now here.
Intriguingly, I see recently on the arXiv:
Previous work has demonstrated that efficient algorithms exist for computing Kan extensions and that some Kan extensions have interesting similarities to various machine learning algorithms. This paper closes the gap by proving that all error minimisation algorithms may be presented as a Kan extension. This result provides a foundation for future work to investigate the optimisation of machine learning algorithms through their presentation as Kan extensions. A corollary of this representation of error-minimising algorithms is a presentation of error from the perspective of lossy and lossless transformations of data.