Category Theory
Zulip Server
Archive

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.

Stream: community: our work

Topic: David Corfield

David Corfield (May 06 2024 at 09:11):

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.

David Corfield (Jun 08 2024 at 09:09):

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!

David Corfield (Aug 14 2024 at 08:16):

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.

John Baez (Aug 14 2024 at 08:54):

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

John Baez (Aug 14 2024 at 09:01):

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.

John Baez (Aug 14 2024 at 09:06):

Anyway, your paper is a lot more well thought-out than this initial reaction! I just couldn't help it.

David Corfield (Aug 14 2024 at 09:17):

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.

John Baez (Aug 14 2024 at 09:45):

Maybe by now you should ask if it's possible for old mathematics to have once had revolutions.

John Baez (Aug 14 2024 at 09:47):

Mac Lane, Eilenberg and Grothendieck are all dead; maybe it's safe for philosophers to start paying attention to them.

David Corfield (Feb 14 2025 at 16:05):

I'm giving a couple of talks next week in Oxford:

• Thurs 20, 14.00, Topos Institute (recorded but not live)

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

• Friday 21, 14.00, OASIS seminar

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.

David Corfield (Feb 14 2025 at 16:07):

I'll be in Oxford from Wednesday 19th. If anyone there would like to chat, then DM me.

John Onstead (Feb 18 2025 at 12:34):

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?

David Corfield (Feb 18 2025 at 13:01):

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:

image.png

I doubt this will satisfy those who seek a single correct interpretation of what's 'really' going on.

David Corfield (Feb 19 2025 at 20:58):

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

David Corfield (Feb 19 2025 at 21:07):

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 $\infty$-category to $\infty-Grpd$ is still an $\infty$-topos. So one start out with HoTT and adjoin various devices, a self-adjoint modality $\natural$, $\otimes$, $\multimap$.

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?

John Baez (Feb 19 2025 at 21:28):

What is the tangent category to $\infty\mathsf{Grpd}$? In other word, does it have some snappy alternative description?

David Corfield (Feb 19 2025 at 22:23):

Parameterized spectra. Fiberwise stabilization of the codomain fibration.

Joyal (who else?) noticed it early.

John Baez (Feb 19 2025 at 22:33):

Nice! I'm amazed, actually, that I understand your answer and it makes perfect sense.

David Corfield (Feb 19 2025 at 22:44):

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 $X$ and a $Y$, but was that part of the May and Sigurdsson story that Mike was responding to?

John Baez (Feb 19 2025 at 22:50):

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.

Mike Shulman (Feb 20 2025 at 01:01):

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.

Mike Shulman (Feb 20 2025 at 01:01):

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.

John Baez (Feb 20 2025 at 01:43):

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!

David Corfield (Feb 20 2025 at 06:22):

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.

David Corfield (Feb 20 2025 at 06:33):

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.

David Corfield (Feb 20 2025 at 06:51):

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

John Baez (Feb 20 2025 at 07:16):

leaving Tom Leinster, Eugenia Cheng and I somewhat mystified.

Yuck!

David Corfield (Feb 20 2025 at 07:17):

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.

David Corfield (Feb 20 2025 at 07:20):

Sounds like we need directed linear HoTT.

David Corfield (Feb 20 2025 at 10:24):

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.

Martti Karvonen (Feb 21 2025 at 09:54):

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?

Mike Shulman (Feb 21 2025 at 11:08):

Framed bicategories and monoidal fibrations, which David mentioned up above.

Fernando Yamauti (Feb 21 2025 at 20:36):

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 $\infty$-category to $\infty-Grpd$ is still an $\infty$-topos. So one start out with HoTT and adjoin various devices, a self-adjoint modality $\natural$, $\otimes$, $\multimap$.

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

David Corfield (Feb 21 2025 at 22:41):

It needs to be an $\infty$-topos, some info here.

So then we're dealing with infinitesimal cohesion. Does that help?

Fernando Yamauti (Feb 21 2025 at 23:11):

David Corfield said:

It needs to be an $\infty$-topos, some info here.

So then we're dealing with infinitesimal cohesion. Does that help?

Ah, yes. By topos I always mean $\infty$-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?

David Corfield (Feb 22 2025 at 13:51):

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:

image.png
image.png

Lane Biocini (Feb 22 2025 at 17:48):

can you point me to this paper?

David Corfield (Feb 22 2025 at 20:27):

This is Mitchell Riley's thesis.

Fernando Yamauti (Feb 22 2025 at 21:10):

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:

image.png
image.png

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 $\mathcal{X}$ seems to be necessarily of the form $\int_{\mathcal{X}} \mathcal{C}$ for $\mathcal{C}$ 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 (?).

Lane Biocini (Feb 22 2025 at 22:29):

David Corfield said:

This is Mitchell Riley's thesis.

thank you!

David Corfield (Feb 23 2025 at 06:39):

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

image.png

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 $\mathbf{H}[X_\ast]$ and $\mathbf{H}^{sec}$.

Also worth noting that one may form the $R$-linear tangent topos for any $E_{\infty}$-ring spectrum, $R$.

Fernando Yamauti (Feb 23 2025 at 22:44):

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 $\mathbf{H}[X_\ast]$ and $\mathbf{H}^{sec}$.

Hmm... So up to presentability issues, it seems models of linear HoTT should be exactly $\int_{\mathcal{X}} \mathcal{C}$ for $\mathcal{C}$ some locus (in the sense of Joyal) with a $0$ 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.

Fernando Yamauti (Feb 23 2025 at 22:48):

David Corfield said:

Also worth noting that one may form the $R$-linear tangent topos for any $E_{\infty}$-ring spectrum, $R$.

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

David Corfield (Feb 24 2025 at 16:46):

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

Fernando Yamauti (Feb 24 2025 at 20:47):

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

Do 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 $R$-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.

David Corfield (Feb 25 2025 at 13:18):

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:

$J^n \mathbf{H} \coloneqq Exc^n(\infty Grpd_{fin}^{\ast/}, \mathbf{H}),$

where the tangent topos is the $1$-jet. And we have from the [[nLab]]:

For $n \in \mathbb{N}$

$Exc^n(\mathcal{C}, \mathcal{D}) \hookrightarrow Func(\mathcal{C}, \mathcal{D})$

for the full sub-$(\infty,1)$-category of the $(\infty,1)$-functor $(\infty,1)$-category on those $(\infty,1)$-functors which are $n$-excisive.

The inclusion is of a left exact reflective sub-$(\infty,1)$-category, hence the inclusion functor has a left adjoint

$P_n \;\colon\; Func(\mathcal{C}, \mathcal{D}) \longrightarrow Exc^n(\mathcal{C}, \mathcal{D})$

which moreover is left exact.

As $n$ ranges, the tower of $n$-excisive approximations of an $(\infty,1)$-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 $[\infty Grpd_{fin}^{\ast/}, \mathbf{H}]$, which is being denoted $\mathbf{H}[X_\ast]$, by $n$-excisive approximations.

David Corfield (Feb 25 2025 at 13:21):

So it's not interpolation to the Sierpinski topos, but to $\mathbf{H}[X_\ast]$.

There's a coreflective inclusion $\mathbf{H}^{\Delta^1} \stackrel{\hookrightarrow}{\longleftarrow} [\infty Grpd_{fin}^{\ast/}, \mathbf{H}] = \mathbf{H}[X_\ast]$ of the Sierpinski topos into the pointed object classifying topos.

David Corfield (Feb 25 2025 at 13:25):

But we then have Urs saying:

Now the Sierpinski topos $\mathbf{H}^{\Delta^1}$ canonically maps to $\mathbf{H}[X_\ast]$, 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 $\infty$-presheaves on the generic section diagram $sec \coloneqq\{id \colon \ast \to x \to \ast\}$, which are bundles $E \to X$ in $\mathbf{H}$ that in addition are equipped with a section. This $\mathbf{H}^{sec}$ does have a fully faithful embedding into $\mathbf{H}[X_\ast]$. And since $sec$ does have a 0-object, $\mathbf{H}^{sec}$ is infinitesimally cohesive over $\mathbf{H}$.

Fernando Yamauti (Feb 26 2025 at 01:36):

David Corfield said:

So it's not interpolation to the Sierpinski topos, but to $\mathbf{H}[X_\ast]$.

There's a coreflective inclusion $\mathbf{H}^{\Delta^1} \stackrel{\hookrightarrow}{\longleftarrow} [\infty Grpd_{fin}^{\ast/}, \mathbf{H}] = \mathbf{H}[X_\ast]$ 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

$\mathbf{H}^{\Delta^1} \rightarrow J^n \mathbf{H} \rightarrow \mathbf{H}[X_\ast]$

or

$\mathbf{H}^{\text{sec}} \rightarrow J^n \mathbf{H} \rightarrow \mathbf{H}[X_\ast]$

where we also have the other $m$-th jet topoi in between (the whole tower).

From what you said, at best, we only get an adjunction

$\mathbf{H}^{\Delta^1} \stackrel{\hookrightarrow}{\longleftarrow} \mathbf{H}[X_\ast]$

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 $n=1$ we only get a factorisation in the "wrong direction"

$J^1 \mathbf{H} \rightarrow {H}^{\Delta^1} \rightarrow \mathbf{H}[X_\ast] .$

David Corfield (Feb 26 2025 at 07:37):

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 $(\infty,1)$-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.

Fernando Yamauti (Feb 26 2025 at 09:53):

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 $(\infty,1)$-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

$\mathbf{H}^{\Delta^{1}} \rightarrow J^n \mathbf{H} \rightarrow \mathbf{H}$

Btw, the rightmost object should be $\mathbf{H}$ in my previous reply (a typo, sorry) and not $\mathbf{H}[X_\ast]$.

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

Fernando Yamauti (Feb 26 2025 at 10:03):

Perhaps you meant to say something like: the Sierpinski topos interpolate between the jet topos and the topos. That means

$J^n \mathbf{H} \rightarrow \mathbf{H}^{\Delta^1} \rightarrow \mathbf{H}$

If so, I do agree. That's completely correct.

What is confusing me is Urs question on what should be $\lim_n J^n \mathbf{H}$. 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.

David Corfield (Feb 26 2025 at 12:19):

OK, that looks right.

And these other toposes? So $\mathbf{H}[X_{\ast}​]$ is just the functor category from which the $n$-jets carve out the $n$-excisive functors.

Then what role is $\mathbf{H}^{sec}$ playing?

Fernando Yamauti (Feb 26 2025 at 14:16):

David Corfield said:

OK, that looks right.

What looks right? I'm confused...

David Corfield (Feb 26 2025 at 17:49):

Fernando Yamauti said:

What looks right? I'm confused...

Sorry, I meant your:

$J^n \mathbf{H} \to \mathbf{H}^{\Delta^1} \to \mathbf{H}$.

Fernando Yamauti (Feb 26 2025 at 19:23):

Ah! Ok. So by interpolation you meant

$J^n \mathbf{H} \to \mathbf{H}^{\Delta^1} \to \mathbf{H} ,$

$J^n \mathbf{H} \to \mathbf{H}^{\text{sec}} \to \mathbf{H}$

and

$J^n \mathbf{H} \to \mathbf{H}[X_*] \to \mathbf{H}$

, 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 (Mar 16 2025 at 19:49):

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:

• @Matthew Pugh, Jo Grundy, @Corina Cirstea, Nick Harris, Learning Is a Kan Extension

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.

David Corfield (Apr 29 2025 at 07:25):

I'm giving a talk today at a workshop, Realism and anti-realism: Paradigms and research programmes in logic and the philosophy of mathematics. It seems to indicate that the date to register even online is passed.

Anyway, slides for The Fivefold Way: Category Theory, Physics, Topology, Logic and Computation, taking off from @John Baez and Mike Stay's Rosetta Stone.

John Baez (Apr 29 2025 at 19:23):

Hey, thanks for giving us a nod. This "quinternity" will become even more powerful if quantum computation ever becomes practical. But even if it's held back by decoherence, the unity of these 5 strands is really exciting.

(Yes, some people do use the word "quinternity", but apparently in a religious context. Besides the 3 usual suspects, the other two are Mary and Satan.)

David Corfield (Apr 30 2025 at 06:09):

Which one would correspond to satan? Weyl once remarked

"In these days the angel of toplogy and the devil of abstract algebra fight for the soul of every individual discipline of mathematics."

Hmm, someone was suggesting I add algebra to make six.

John Baez (Apr 30 2025 at 06:31):

By the way, in the Rosetta Stone paper we didn't treat category theory as living on an equal footing with physics, topology, logic and computation: instead it was presented as a way to see a strong analogy between (certain aspects of) the other four subjects.

David Corfield (Apr 30 2025 at 09:02):

Yes, I discussed that. The Trinitarians then move in a more democratic direction.

It's hard enough to get any audience for CT among philosophers. Offering them an equal say for logic is a diplomatic move.

Seems to be my role these days, the token CT-ist.

John Baez (Apr 30 2025 at 20:57):

You're just a bit ahead of your time. In another 2000 years, philosophers will be as interested in category theory as they are in Aristotle now.

David Corfield (May 02 2025 at 11:46):

Something that's confusing me a little in my passage from following the Sati-Schreiber program to working in an ACT setting is that, although the natural direction in many ACT projects would appear to be to increase the homotopical level, there seems to be a certain inertia.

A couple of examples where the step is being indicated:

• David Spivak and C.B. Aberlé Polynomial universes and natural models

We shall see how the language of polynomial functors can be used to elegantly capture all of the usual constructs of dependent type theory, and moreover, how interpreting this language in homotopy type theory reveals striking properties of these structures.

• Joachim Kock

Although the field of Petri net theory is very much driven by applications — in computer science,
natural sciences, and industry — the present work is motivated by theoretical interest. Up to the
point developed here, I think the theoretical picture is quite satisfactory and clean, at the price
of some homotopy overhead. It is my opinion that Petri-net theorists and end users can bargain
against this price in various ways (see [26] for some explicit bargaining), which I think amounts
to falling back on previous approaches. It is my hope nevertheless that the account given here will
resonate with modern trends in theoretical computer science, and with homotopy type theory [65]
in particular, where specified bijections are part of the whole set-up in the form of terms of identity
types.

But why the need for the bargaining? Is it so very costly?

This morning I was taking a look around a bunch of related constructions: Combinatory Homomorphic Automatic Differentiation, lenses, dialectica categories, and so on. The meander culminated in the interesting paper

• Fernando Lucatelli Nunes and @Matthijs Vákár, Monoidal closure of Grothendieck constructions via $\Sigma$-tractable monoidal structures and Dialectica formulas

This looks to study the "categorical structure of the Grothendieck construction of an indexed category and characterise fibred limits, colimits, and monoidal structures". Again, there's a pointer to some higher homotopical levels in one example:

Example 26 (Indexed groupoids). Hofmann and Streicher (1998) restricts Example 25 to indexed groupoids indexed by another groupoid. That gives us another model of dependent type theory and it is the starting point for homotopy type theory, where people consider variants of this model based on ∞-groupoids rather than 1-groupoids [Kapulkin and Lumsdaine (2021)].

I guess my trajectory must be odd. It feels like descending to a truncated shadow of where one once was, a place where things just work out very pleasantly. From where I began, the pinnacle of the $(\infty)$-Grothendieck construction yielding good structure was the surprising result that the tangent $\infty$-category of an $\infty$-topos is still an $\infty$-topos, the result that makes linear HoTT tick.

I get that it's important to work out what happens over a range of structures of varying strengths, but is it not good to keep an eye on both ends of the range? It's not as though commitment to linear HoTT forces you to only consider high-end Lurie-esque stable homotopy theory/spectral algebraic geometry. In The Quantum Monadology it's being used to depict quantum measurement processes in the setting of good old low-level finite-dimensional vector spaces.

So there's my puzzlement. Along with Joachim's "homotopy overhead", why not consider what might be called the "truncation overhead"? For an example of the latter, see this discussion of a case where things are easier at the top of the ladder.

John Baez (May 02 2025 at 13:16):

David Corfield said:

Something that's confusing me a little in my passage from following the Sati-Schreiber program to working in an ACT setting is that, although the natural direction in many ACT projects would appear to be to increase the homotopical level, there seems to be a certain inertia.

The great advantage of doing applied mathematics is that your work directly helps people doing practical things outside mathematics. The flip side is that you either have to explain what you're doing to these practitioners, and convince them that it's worth taking the time to understand the math you're using, or else create software that black-boxes the math so that the practitioners can use the software without understanding exactly how it works. In the latter case you still need to explain how to use the software, which is nontrivial if it does anything new.

For example, there's a tradition called System Dynamics which uses 3 different diagram languages to model complex systems; it's widely used in business, economics and epidemiology. There are existing commercial software packages that let practitioners build system dynamics models. A bunch of us are trying to build free software that's better, using category theory. So far it's taken about 15 years to:

• develop the underlying categorical concepts, working very hard to keep them as simple as possible and explain them to as many people as possible;
• find computer scientists who understand and like category theory enough for them to put years into developing a software platform capable of supporting the categorical concepts in a clean way;
• find a system dynamics practitioner who understands and like category theory enough that they decided to use this software in their work, and devote their career to developing it further.

The project still has a long way to go! It'll count as a success when a lot of epidemiologists - or perhaps other system dynamics practitioners, but so far it's looking like epidemiologists - regularly use our software and its new capabilities.

We're in a pretty good position. If I accidentally made it sound like this project is mainly about me, that would be completely misleading. As you probably know, James Fairbanks and Evan Patterson led development of AlgebraicJulia, a software environment suited to categorical constructions including presheaf categories and structured cospans. Then Nate Osgood, who is both a computer scientist and epidemiologist, and knows category theory, became deeply involved in the software development. He's starting to use the software in his many courses, which appear on YouTube. He's also using in his epidemiological research. Then Brendan Fong, who helps lead the Topos Institute, has embraced this project. And there are lots of other important people I'm not naming here.

But success is still far from guaranteed! We still haven't gotten any epidemiologists to switch from the commercial software to our new free software... except perhaps the kids who are taking Nate's courses, who are still just students. And so on.

In this sort of situation, any increase in abstraction has a big cost that needs to be justified by practical benefits.

Given all this, I just don't see that 'increasing h-levels' is a reasonable priority in this particular project. It's obviously crossed my mind, but there are so many other things that have a bigger bang for the buck.

I was actually amazed that the more practical members of this project embraced double categories. They're still not incorporated in the AlgebraicJulia software - and while they play a fundamental role in the new CatColab software, they're so far being used in their role to formulate 'double categorical doctrines', not double categories of open systems. But I'm hoping that someday we'll be using them in software for epidemiology. Maybe 5 more years?

David Corfield (May 02 2025 at 16:37):

Thanks! There's obviously a complicated ecosystem of communities. I can see great inertia arising from the practical end of the chain, but I think the question was more about the theoretical end addressing each other.

Still, would it be such a stretch to have your $\Sigma$-nets deployed, if Joachim's whole-grain nets are already?:

image.png

Is there much more for developers to worry about from anything extra here?:

image.png

John Baez (May 02 2025 at 18:28):

I've never yet felt any desire in my own work to use $\Sigma$-nets. For chemistry I was perfectly happy with old-school Petri nets. But AlgebraicJulia is designed to exploit presheaf categories, so it favors whole-grain Petri nets.

If for some reason I were really concerned about situations where a mix of the "collective token philosophy" and "individual token philosophy" were important, then I'd need $\Sigma$-nets.

(When I first discussed this with Joachim he joked that he didn't do philosophy. He hadn't read the discussions about these two attitudes toward the nature of tokens in Petri nets. It sounds like now he gets the point.)

David Corfield (May 03 2025 at 06:29):

John Baez said:

But AlgebraicJulia is designed to exploit presheaf categories, so it favors whole-grain Petri nets.

Huh? I thought $\Sigma$-nets form a presheaf category. Joachim seems to think so:

image.png

image.png

image.png

John Baez (May 03 2025 at 07:52):

Okay, maybe it is! It shows how little I've thought about $\Sigma$-nets. Let me say more clearly what I really meant.

People who work with Petri nets in AlgebraicJulia take advantage of the fact that a whole-grain Petri net is just a set of states $S$, a set of transitions $T$, a set of input wires $I$, a set of output wires $O$, and functions $I \to S$, $I \to T$, $O \to S$, $O \to T$. It's super-easy to deal with that data structure.

$\Sigma$-nets are considerably more complicated, writing software to deal with them looks harder, and nobody has yet found a reason to do it. I imagine that happening only if people start wanting Petri nets that give you control over when you take the collective token philosophy (tokens have no individual distinctiveness so permuting them doesn't matter), when you take the individual token philosophy (permuting them does), and when you want something in between (some permutations count as doing something, others don't).

David Corfield (May 03 2025 at 09:31):

John Baez said:

when you want something in between (some permutations count as doing something, others don't).

Right, that was your selling point

image.png

There's a lovely account of what amounts to the "homotopy overhead" of whole-grain and $\Sigma$-nets in

• Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis, The Univalence Principle

image.png

Presumably @Mike Shulman as the common author had a large hand in this section. So I guess I'm left wondering how much harder it is to program with such data structures, but I probably need a course in programming to get a feel for it.

John Baez (May 03 2025 at 11:28):

Right, that was your selling point

Yeah, it's like that album by Megadeth: Peace Sells... But Who's Buying? Even I, one of the authors of the paper on $\Sigma$-nets, have never dreamt of using them for anything.

John Baez (May 03 2025 at 11:47):

So I guess I'm left wondering how much harder it is to program with such data structures...

It's harder, so the question is whether anyone cares about what they can do. In our paper I considered them merely as the answer to this natural question: what should go in the bottom middle of this diagram?

John Baez (May 03 2025 at 11:49):

Prenets present free strict monoidal categories, Petri nets present free commutative monoidal categories, what presents free strict symmetric monoidal categories?

John Baez (May 03 2025 at 11:50):

$\Sigma$-nets may have their day in the sun if people ever work with Petri nets in a programming framework that natively supports homotopy type theory.

Kevin Carlson (May 03 2025 at 20:03):

This is a bit of a lazy question, but would anyone care to give a short sentence about why there’s homotopy theory needed in $\Sigma$-nets? I’ve never gotten very far in reading about this properly and it doesn’t seem to come out of the conversation above yet.

David Corfield (May 04 2025 at 06:29):

Kevin Carlson said:

a short sentence about why there’s homotopy theory needed in $\Sigma$-nets?

From that passage of Benedikt Ahrens et al. The Univalence Principle I cited above, it seems to amount to a non-free action meaning some type has hlevel 1.

John Baez (May 05 2025 at 10:38):

This seems to confirm my guess that the "homotopy theory" needed for $\Sigma$-nets is really just "homotopy 1-type theory", aka groupoid theory. That's good if there is resistance to higher h-levels, as there certainly is among many.