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.
Evan Patterson (Mar 18 2023 at 06:47):OK, I'm going to give this a shot.
Two things that I just finished doing:
Evan Patterson (Mar 18 2023 at 06:50):Some things that I'm currently working on:
John Baez (Mar 19 2023 at 01:51):What'll the focus be for your ACT2023 paper? I'm always interested in structured and decorated cospans, and I gave two talks about them at ACT2022: one about turning structured cospans into decorated cospans, and another about StockFlow.jl.
John Baez (Mar 19 2023 at 01:55):Thid time I might try to talk about ModelCollab, our new graphical user interface for StockFlow.jl, and some of the new math we came up with to give different choices of semantics for stock-flow duagrams.
Evan Patterson (Mar 19 2023 at 06:57):John Baez said:
Thid time I might try to talk about ModelCollab, our new graphical user interface for StockFlow.js, and some of the new math we came up with to give different choices of semantics for stock-flow duagrams.
Cool. I've been meaning to dig into that long new paper you wrote with Xiaoyan and others. Would be great to hear a talk about it.
Evan Patterson (Mar 19 2023 at 06:58):BTW, I think you mean StockFlow.jl, although as a web application, ModelCollab must have a JavaScript implementation of stock-flow diagrams one way or another.
Evan Patterson (Mar 19 2023 at 07:05):John Baez said:
What'll the focus be for your ACT2023 paper?
The overall idea is to argue that using more concepts from double category theory is helpful for understanding structured and decorated cospans. The paper will be mostly based on two blog posts that I wrote over the past year or so. The recent post, linked above, is about how structured cospans form a cocartesian double category, the doube-categorical analogue of a cocartesian category.
Evan Patterson (Mar 19 2023 at 07:09):Previously, I wrote a blog post about how decorated cospans can be derived as an application of the double Grothendieck construction. It's actually quite straightforward---the point is that, until very recently, nobody knew what the double Grothendieck construction was! (Or, at least, if people knew, it wasn't published anywhere.)
Morgan Rogers (he/him) (Mar 19 2023 at 09:18):@Nicolas Blanco have a talk about that Grothendieck construction recently, amongst others, it's exciting to learn that it's already got applications!
John Baez (Mar 19 2023 at 18:22):Yes, I meant .jl. Fixed.
Evan Patterson said:
John Baez said:
The overall idea is to argue that using more concepts from double category theory is helpful for understanding structured and decorated cospans. The paper will be based mostly on two blog posts that I wrote over the past year or so. The recent post, linked above, is about how structured cospans form a cocartesian double category, the double-categorical analogue of a cocartesian category.
John Baez (Mar 19 2023 at 18:23):Great! The way that Kenny Courser and I proved structured cospans are a symmetric monoidal double category used something like the fact that they're a cocartesian double category.
John Baez (Mar 19 2023 at 18:24):As you know, double categories are "weak category objects" in Cat - that is, like category objects, but where composition is associative and unital only up to isomorphisms, which in turn obey equations like the pentagon identity.
John Baez (Mar 19 2023 at 18:27):We showed that structured cospan category objects are better: they are weak category objects in Rex, the 2-category of categories with finite colimits. And we said this would be important!
But then we went ahead and showed they are also weak category objects in SymmMonCat, the 2-category of symmetric monoidal categories. (This is easy.) And using that, we showed they are symmetric monoidal double categories. (This is almost easy.)
John Baez (Mar 19 2023 at 18:29):When you say "cocartesian" do you mean "with finite coproducts" or "with finite colimits"? I could check, but I'm too lazy. I hope you mean the latter, and I bet you do, because that's much more useful for applications: it lets you "glue together" models of open systems.
Evan Patterson (Mar 19 2023 at 21:15):John Baez said:
We showed that structured cospan category objects are better: they are weak category objects in Rex, the 2-category of categories with finite colimits. And we said this would be important!
Right, that does seem important! I would like to understand how that statement is related to having certain double-categorical colimits. I'm sure there is some connection.
Evan Patterson (Mar 19 2023 at 21:17):John Baez said:
When you say "cocartesian" do you mean "with finite coproducts" or "with finite colimits"? I could check, but I'm too lazy. I hope you mean the latter, and I bet you do, because that's much more useful for applications: it lets you "glue together" models of open systems.
I actually mean finite double-categorical coproducts, which are sufficient to get a symmetric monoidal double category (just like finite coproducts are sufficient to get a symmetric monoidal category). I prove this under the assumption that the functor preserves finite coproducts. Under stronger assumptions, it is probably possible to prove something stronger.
Nathanael Arkor (Mar 19 2023 at 23:10):I actually mean finite double-categorical coproducts, which are sufficient to get a symmetric monoidal double category
Is there a reference for this already?
Evan Patterson (Mar 20 2023 at 04:26):That is a fair point. I don't know a reference for this statement. So, as it stands, there is a little gap in my argument. I suppose I might have to write out a proof, although I'd really prefer to cite something instead.
Evan Patterson (Mar 20 2023 at 06:01):On second thought, this should be true by abstract nonsense. A (co)cartesian double category can be defined as a (co)cartesian object in , whereas a symmetric monoidal double category is a symmetric pseudomonoid in . So it would suffice that for any 2-category with finite 2-products, a (co)cartesian object in is automatically a symmetric pseudomonoid in in a canonical way.
Now I don't have a literature reference for that claim either, but the nLab page for cartesian object says that it is true (although it doesn't specifically say "symmetric"). I would be grateful if anyone could provide a reference.
Nathanael Arkor (Mar 20 2023 at 12:28):Considering only 2-categories of double categories will impose only a 1-dimensional monoidal structure, akin to a monoidal category rather than a monoidal bicategory. I would have expected it to be necessary to consider monoids in 3-categories instead, since a monoidal double category generalises a monoidal bicategory. (Though this depends on exactly how weak one needs the monoidal structure to be.)
Evan Patterson (Mar 20 2023 at 21:44):You might want to have a look at the appendix to the Baez-Courser paper, which helpfully unpacks the definition of a pseudomonoid in . In essence, this gives: the structure of a weak monoidal product on each of the underlying categories of the double category, which are strictly preserved by the source and target functors, along with coherent isomorphisms interchanging the monoidal product and unit with the external composition. IMO, this is the amount of weakness you would expect to have in a monoidal double category.
Nathanael Arkor (Mar 20 2023 at 22:23):Okay, I see, that's a stricter notion than I was expecting (i.e. asking for structural isomorphisms rather than structural equivalences). I don't know of a reference for cartesian objects being pseudomonoids.
John Baez (Mar 21 2023 at 00:49):Evan Patterson said:
On second thought, this should be true by abstract nonsense. A (co)cartesian double category can be defined as a (co)cartesian object in , whereas a symmetric monoidal double category is a symmetric pseudomonoid in . So it would suffice that for any 2-category with finite 2-products, a (co)cartesian object in is automatically a symmetric pseudomonoid in in a canonical way.
Now I don't have a literature reference for that claim either, but the nLab page for cartesian object says that it is true (although it doesn't specifically say "symmetric"). I would be grateful if anyone could provide a reference.
I don't know a reference, but I think you can prove the abstract fact "by hand", very much like how Kenny and I argue there's a strict 2-functor from Rex to SymmMonCat. Our same argument would show there's a strict 2-functor from Cocart to SymmMonCat, and you can undoubtedly show more generally there's one from the 2-category of cocartesian objects in to the 2-category of symmetric pseudomonoids in .
John Baez (Mar 21 2023 at 00:52):Of course it would be nice if someone had already proved this, but even we category theorists need to do actual work. :upside_down:
John Baez (Mar 21 2023 at 00:57):My main comment here is that if "cocartesian object" (like coproduct) is defined by a universal property, you'll probably have to make a choice to turn a cocartesian object into a symmetric pseudomonoid. Well, I can at least say this for sure: need to choose coproducts to turn a cocartesian category into a symmetric monoidal category!
Mike Shulman (Mar 21 2023 at 00:57):I guess this is probably one of those facts that is so obvious to to an Australian that no one has ever felt the need to write it down. You can probably deduce it from the case of categories and the Cat-enriched Yoneda lemma.
John Baez (Mar 21 2023 at 00:59):So yeah, you can include a reference saying "Obvious in Australia."
John Baez (Mar 21 2023 at 01:29):But seriously, I think it's good to really prove these highly believable facts, both in order to be honest and so that future mathematicians have an actual proof to point to.
John Baez (Mar 21 2023 at 01:30):I've been doing a lot of that these days, to pay off my debt to society.
Evan Patterson (Mar 21 2023 at 05:49):John Baez said:
My main comment here is that if "cocartesian object" (like coproduct) is defined by a universal property, you'll probably have to make a choice to turn a cocartesian object into a symmetric pseudomonoid. Well, I can at least say this for sure: need to choose coproducts to turn a cocartesian category into a symmetric monoidal category!
Right! Being a cocartesian object means that certain left adjoints exist, but in order to get a pseudomonoid, you'll have to make a choice for those adjoints, which are only unique up to canonical isomorphism.
Evan Patterson (Mar 21 2023 at 05:53):Mike Shulman said:
I guess this is probably one of those facts that is so obvious to to an Australian that no one has ever felt the need to write it down. You can probably deduce it from the case of categories and the Cat-enriched Yoneda lemma.
Alas, I am not an Australian (much less the right kind of Australian). While this fact seems highly plausible to me based on the analogy to , it is not immediately obvious to me how to prove it. So I suppose I had better do it.
Matteo Capucci (he/him) (Mar 23 2023 at 10:29):What Mike is saying is that if your ambient 2-category is structured enough (I suspect you need just monoidal structure...), the proof of this fact in Cat, using objects and arrows, carries over formally to , by- the aforementioned variant of the Yoneda lemma.
Mike Shulman (Mar 23 2023 at 15:21):I think in this case what you need is that has finite products.
Evan Patterson (Mar 23 2023 at 17:01):Thanks both. I'll have to think about that.
Nathanael Arkor (Mar 23 2023 at 18:17):Evan Patterson said:
Mike Shulman said:
I guess this is probably one of those facts that is so obvious to to an Australian that no one has ever felt the need to write it down. You can probably deduce it from the case of categories and the Cat-enriched Yoneda lemma.
Alas, I am not an Australian (much less the right kind of Australian). While this fact seems highly plausible to me based on the analogy to , it is not immediately obvious to me how to prove it. So I suppose I had better do it.
The basic idea would be something like this. Suppose you have a 2-category with finite 2-products, and a cartesian object therein. Then is a cartesian object in the 2-presheaf 2-category, because 2-functors preserve adjunctions and the 2-Yoneda embedding preserves 2-products. This means that is a cartesian object in Cat for each object , i.e. a cartesian category, and hence a monoidal category, i.e. a pseudomonoid in Cat. Consequently, is a pseudomonoid in the 2-presheaf 2-category. Finally, since the 2-Yoneda embedding is locally fully faithful, it reflects pseudomonoids, so that is a pseudomonoid in .
John Baez (Mar 23 2023 at 22:44):Thanks for spelling it out, @Nathanael Arkor!
Evan Patterson (Mar 23 2023 at 23:52):Yes, that's very helpful. Thanks!
Evan Patterson (Mar 30 2023 at 03:03):@Nathanael Arkor, I took the liberty of transcribing your proof on the nLab for cartesian object. Hopefully I didn't mangle it too badly!
John Baez (Mar 31 2023 at 07:01):The proof of the new Proposition 2.1 says that each cartesian object C(Y,X) in Cat is "canonically" a symmetric pseudomonoid for each Y C but not does not mention that that for each Y we need to choose a way to make the cartesian category C(Y,X) into a symmetric monoidal category. Earlier the article says
By making a choice of products, any category with finite products is automatically a symmetric monoidal category in a canonical way.
without saying what it means for A to be canonically B "by making a choice". "Canonically" is not the most precise term in the big book of math, but usually it connotes that you don't need to make an arbitrary choice.
John Baez (Mar 31 2023 at 07:06):The concept of a property-like structure is relevant here.
Nathanael Arkor (Mar 31 2023 at 07:38):Yes, it should really be "a cartesian object with specified right adjoints" (rather than merely asking that they exist).
Mike Shulman (Mar 31 2023 at 14:51):The thing is that these "choices" are not really "choices" from a categorical point of view, since they are unique up to unique isomorphism. In a foundational theory that understands this, like HoTT/UF, no choice is actually required, for essentially the same reason that no choice is required in a set-theoretic foundation to make "choices" that are literally unique. So while I agree the situation could be described more clearly, I would argue that this structure is canonical.
John Baez (Mar 31 2023 at 14:51):Nathaniel wrote:
Yes, it should really be "a cartesian object with specified right adjoints" (rather than merely asking that they exist).
Right. But then one can show the 2-category of cartesian objects (with suitably defined morphisms and 2-morphisms) is equivalent to the 2-category of cartesian objects with specified right adjoints (with suitably defined morphisms and 2-morphisms, where the morphisms are compatible with the right adjoints but do not need to preserve the specified right adjoints on the nose).
John Baez (Mar 31 2023 at 14:55):It takes a bit of work to state this (as hinted in my parenthetical remarks), but when we're done we've formalized our intuition that the choice of right adjoints to and "doesn't really matter".
John Baez (Mar 31 2023 at 19:50):@Mike Shulman wrote:
In a foundational theory that understands this, like HoTT/UF, no choice is actually required, for essentially the same reason that no choice is required in a set-theoretic foundation to make "choices" that are literally unique. So while I agree the situation could be described more clearly, I would argue that this structure is canonical.
Yes, this is a great example of where using better foundations eliminates a lot of hassle. My previous comment, in case it wasn't obvious, was for category theory founded on traditional set-theoretic foundations (ZFC or whatever).
John Baez (Mar 31 2023 at 20:03):I think it's good to work out this problem quite clearly using traditional set-theoretic foundations even if the main result is to push you into the arms of HoTT.
John Baez (Mar 31 2023 at 22:13):So, you see, @Evan Patterson, that this is issue, while not incredibly complicated, is still subtle enough that people start talking about different foundations of mathematics!
John Baez (Mar 31 2023 at 22:20):The point of using other foundations here is simply to avoid suffering over the issue that a cartesian category can be made into a symmetric monoidal category in many ways, but for any pair of these ways we have a chosen isomorphism between them.
If you think of the ways as forming a set, it's a big set. But if you think of them together with these isomorphisms as forming a groupoid, this groupoid is 'contractible': in other words, it's equivalent to the groupoid with one object and one morphism.
So, using better foundations, we say there's just one way.
Evan Patterson (Mar 31 2023 at 23:50):Thanks! I take your point about the subtleties here. And, even apart from the foundational aspects, I see why it would be jarring to say "make a choice" and then immediately say the construction is "canonical." I tried to revise what I wrote on nLab to avoid this confusion. What do you think?
Evan Patterson (Mar 31 2023 at 23:53):It's actually annoying enough to make me appreciate why you might want another foundation!
John Baez (Mar 31 2023 at 23:55):This looks a lot better! Getting down into tiny details, I think this phrase could be polished:
a cartesian object in the 2-category of 2-presheaves on C with a choice of right adjoints
since "with a choice of right adjoints" superficially seems to apply to "2-presheaves". So maybe try this:
a cartesian object with a choice of right adjoints in the 2-category of 2-presheaves on C
John Baez (Apr 01 2023 at 00:00):Anyway, it's pretty interesting how "applied" category theory can force one to pay attention to such sneaky issues.... at least until one understands them well enough to say "okay, I get it, I don't need to talk about it!" :upside_down:
Evan Patterson (Apr 01 2023 at 00:17):Good point. I cleaned up that phrasing.
Evan Patterson (Apr 01 2023 at 00:18):John Baez said:
Anyway, it's pretty interesting how "applied" category theory can force one to pay attention to such sneaky issues.... at least until one understands them well enough to say "okay, I get it, I don't need to talk about it!" :upside_down:
Here I was, just innocently trying to claim that a cocartesian double category is canonically a symmetric monoidal double category :)
John Baez (Apr 01 2023 at 00:44):Just put quotes around "is" and "canonically" and you're fine. :thumbs_up:
John Baez (Apr 01 2023 at 00:45):Or, if you join HoTT, you can remove the quotes.
John Baez (Apr 01 2023 at 00:50):It just costs $8 per month.
Evan Patterson (Apr 01 2023 at 00:53):I would pay $8/month to make my vague statements be meaningful and correct!
John Baez (Apr 01 2023 at 00:56):I'd pay a lot more, but unfortunately HoTT doesn't handle most of my vague statements.
Evan Patterson (Apr 05 2023 at 04:43):A few updates:
Updated the biochemical regulatory networks on arXiv and submitted it for publication.
Besides various minor revisions in response to feedback, this version has several new substantial examples.
Submitted to arXiv a new paper about structured and decorated cospans.
This is the work that motivated the recent discussions in this thread. Thanks a bunch to everyone who helped me with the 2-categorical issues lurking in the background!
John Baez (Apr 05 2023 at 15:59):Where did you submit the biochemical regulatory networks paper? (You can whisper it in my ear if you don't want to reveal it publicly.)
John Baez (Apr 05 2023 at 15:59):I'm just always curious about where to submit papers like this.
Evan Patterson (Apr 06 2023 at 03:27):I'm never quite sure how open to be about such things---best not to count your chickens until they're hatched---but I'll go ahead and say that we submitted it to Compositionality. My coauthors and I had a long discussion about where to submit it, with the main contenders being Compositionality or a mathematical biology journal. I like the idea of writing for scientists in the application domain, and I was pleased that a recent paper on diagrammatic differential equations got accepted in an engineering mathematics journal, but in this case we felt that the emphasis on the category theory was too high for the math bio journals that we were looking at. We have hopes of writing another paper with less category theory and more simulation and submitting that to a math bio journal, but work on that project has not even started.
Evan Patterson (Apr 06 2023 at 03:29):In general, I struggle a lot with the question of where to submit papers like this and I don't have any clear principles about how to make the decisions. There is, of course, always a lot of uncertainty about what kind of reviewers you'll get.
Evan Patterson (Apr 06 2023 at 03:32):I've noticed that you've published a number of CT-heavy papers in the Journal of Mathematical Physics over the years, so there must be somebody there tolerant of category theory :)
John Baez (Apr 06 2023 at 05:14):I often try to publish applied category work in non-categorical journals because I figure it increases the credibility of category theory, and also my work, among people who work in those other subjects. To put it simplistically, publishing a paper about categories of open Markov processes in Journal of Mathematical Physics signals "now mathematical physicists are getting interested in using categories to study Markov processes", while publishing the same paper in a category theory journal signals "now category theorists are getting interested in using categories to study Markov processes" - and I find the former message more exciting and useful.
John Baez (Apr 06 2023 at 05:17):But I still publish a lot in TAC and a bit in Compositionality. I feel limited in how much I publish in Compositionality because I'm on the steering board of that journal. But I feel publishing there a bit is important because I'd hate to be perceived as shunning it!
Evan Patterson (Aug 15 2023 at 23:15):I wrote a blog post on unbiased monoidal categories and unbiased SMCs: Unbiased monoidal categories are pseudo-elements
The main idea is that the observation that multicategories already "know about" monoids can be categorified to recover pseudomonoids, and in particular monoidal categories, from 2-multicategories. The monoidal categories that you get are unbiased. But, as I argue in the post, I think that's actually good!
Cole Comfort (Aug 16 2023 at 00:05):deleted message, I saw that you already read the brilliant paper of Hermida
Jean-Baptiste Vienney (Aug 16 2023 at 00:32):Loved that blog post! It feels good to see a definition of symmetric monoidal category with diagrams which don't seem to come from nowhere -- contrary to the usual coherence diagrams.
Evan Patterson (Aug 16 2023 at 00:49):Cole Comfort said:
deleted message, I saw that you already read the brilliant paper of Hermida
Yes, it was by reading Hermida's paper "Representable multicategories" that I came to appreciate why multicategories are such a natural concept. Nowadays I'm trying to use multicategories by default when both multicategories and monoidal categories would work, but of course sometimes you actually do need a monoidal category, namely when you need to map into a product.
Cole Comfort (Aug 16 2023 at 08:46):Evan Patterson said:
Cole Comfort said:
deleted message, I saw that you already read the brilliant paper of Hermida
Yes, it was by reading Hermida's paper "Representable multicategories" that I came to appreciate why multicategories are such a natural concept. Nowadays I'm trying to use multicategories by default when both multicategories and monoidal categories would work, but of course sometimes you actually do need a monoidal category, namely when you need to map into a product.
Well you could also use poly categories, then you can have an unbiased view of monoidal categories in the input and in the output... although you can't cut along more than one wire at a time. What I really want is a structure where you have this unbiased notion of tensor product, and you can cut along multiple wires at the same time, so that the appropriate notion of pseudofunctor 1->Prof would be coherent structure of unbiased (cauchy complete) monoidal category, and the grothendieck construction of which would be essentially a strict monoidal category. If multicategories categorify monoids, and poly categories categorify frobenius monoids, then what is the appropriate categorification of special frobenius monoids
Nathanael Arkor (Aug 16 2023 at 09:24):What I really want is a structure where you have this unbiased notion of tensor product, and you can cut along multiple wires at the same time
This is the notion of a [[properad]]. If you permit composition along "no wires", then you get the notion of a [[PROP]].
Mike Shulman (Aug 16 2023 at 14:57):Or "colored prop" for emphasis. Unlike in the case of operads / multicategories and dioperads / polycategories, in the case of props there doesn't seem to be a different word for the multi-object case.
Evan Patterson (Oct 10 2023 at 04:38):I'm happy to say that my paper with Michael Lambert on Cartesian double theories: A double-categorical framework for categorical doctrines is finally out on arXiv.
The paper isn't as scary its length might suggest :) It's long because we have a lot of examples and we try to present the definitions and proofs with attention to the details, but the main idea can be stated in one sentence: we combine cartesian double categories and lax double functors to formalize doctrines using double-categorical functorial semantics. A cartesian double theory is thus a kind of categorified algebraic theory.
Mike Shulman (Oct 10 2023 at 16:00):Nice!
If I were you I would be a less deprecating of presentations of 2-monads. There's a notion of 2-Lawvere theory, for instance, that I don't think is substantially more complex than ordinary Lawvere theories, and also plenty of other technology for presenting 2-theories such as operads, clubs, cartesian 2-multicategories, etc.
On a quick glance it looks like many of your examples have theories that are actually cartesian 2-categories, i.e. finite product 2-theories. What are some examples of double theories that don't fit into that framework?
Kevin Arlin (Oct 10 2023 at 16:50):Is it actually in the literature somewhere how any of these notions present 2-monads, though? I admit I haven't read all Kelly's papers on clubs but that's older than the main 2-monad papers, anyway...The only literature I'm aware of on 2-Lawvere theories is a few words in Bourke's "flexible aspects", and if you could import some straight enriched category theory to get the free 2-monad on a 2-Lawvere theory without working for it you'd still surely have to work to understand whether the two pictures give the same pseudo and lax morphisms, etc. (Besides, I'm pretty sure you don't get this from the plain enriched case; Jason Parker just put up a preprint today that should be state of the art, but only handles cartesian closed enrichment bases generated by the terminal object.) Maybe you and Riley and Licata do something about this somewhere in your project?
Evan Patterson (Oct 10 2023 at 17:21):Mike Shulman said:
On a quick glance it looks like many of your examples have theories that are actually cartesian 2-categories, i.e. finite product 2-theories. What are some examples of double theories that don't fit into that framework?
Thanks for your questions/comments. You're right that a decent number of the theories are actually 2-categorical. These theories have a nice property: they always give a (pseudo) double category of models, rather than merely a virtual one. But we also consider quite a few theories that aren't of this form. One that I like quite a bit is the "theory of promonoids" (Theory 6.8), whose (lax) models are multicategories. This theory isn't "2-categorical," although one might say that it is "bi-categorical." For an example using everything available in a double theory, see Theories 6.11 and 6.12, whose models are (symmetric) monoidal copresheaves. This example is extended further in Theory 6.15.
Evan Patterson (Oct 10 2023 at 17:27):Mike Shulman said:
If I were you I would be a less deprecating of presentations of 2-monads.
Thanks, I'll be more careful in my phrasing; I don't want to annoy people. It would be helpful to know, though, if I'm missing something: my understanding of what is "a presentation of a 2-monad" comes from Sec 5 of Lack's helpful expository paper, "A 2-categories companion." Is there any other notion of presentation that you have mind? In that regard, I share Kevin's questions.
Nathanael Arkor (Oct 10 2023 at 17:46):There are several different approaches, but one convenient method is via enriched theories. For instance, Bourke and Garner show how to present a 2-monad for monoidal categories in Example 13 of Monads and theories, while Lucyshyn-Wright and Parker do the same using slightly different techniques in Example 6.2 of Diagrammatic presentations of enriched monads and varieties for a subcategory of arities.
Evan Patterson (Oct 10 2023 at 17:49):Thanks! It should be illuminating to see how the 2-monad for monoidal categories is presented using these approaches.
Kevin Arlin (Oct 10 2023 at 18:55):Ah, those are very interesting papers, which disprove my parenthetical about whether you can present a good notion of 2-theory using enriched category theory, thanks!
As far as I can tell these two papers only define, for instance, the 2-category of monoidal categories and strict monoidal functors directly as models of their theories. Thus you'd have to pass to the associated 2-monad to get your hands on a notion of pseudo, lax, and oplax morphisms. I'd argue that gap means that these just are not actually theories of 2-theories, and more than the theory of cat-enriched monads is the theory of 2-monads, though it's clearly a very useful start.
Evan Washington (Oct 10 2023 at 19:19):Great! Really excited to read this!!
Wanted to point you to this, which I didn't see a reference to in the paper at a glance: Paré has a few lecture notes on treating coherent first-order theories as 'double Lawvere theories' which seem to be the same sort of thing except (a) Paré's double Lawvere theories have 'local coproducts' and so may be more properly called 'coherent double theories' and (b) models are strong rather than lax double functors.
I also have lots of questions, like: Do you see prospects for going in the other direction on the hierarchy of categorical logics? e.g. should there be some useful notions of double Markov categories?
Nathanael Arkor (Oct 10 2023 at 19:46):Kevin Arlin said:
I'd argue that gap means that these just are not actually theories of 2-theories, and more than the theory of cat-enriched monads is the theory of 2-monads, though it's clearly a very useful start.
Yes, I agree with this, but I think the phrase Mike was objecting to was "By contrast, there is no simple way to present a 2-monad". Certainly presentations are only part of the story, but I think it is reasonable to say there are simple ways to present 2-monads.
Evan Patterson (Oct 10 2023 at 21:26):I seem to have a different calibration for what is "simple" but the point is well taken: I will find another way to make the comparison that doesn't depend on anyone's opinion about what is or isn't simple.
Evan Patterson (Oct 10 2023 at 21:48):Evan Washington said:
Great! Really excited to read this!!
Wanted to point you to this, which I didn't see a reference to in the paper at a glance: Paré has a few lecture notes on treating coherent first-order theories as 'double Lawvere theories'...
Thanks for the comment and the pointer! At one point I looked through these slides enough to convince myself that it was an appreciably different story, although there are certainly similarities too. I agree that it would be helpful to include a comparison in the paper.
As I understand it, Pare's story is related to the one that @Christian Williams has been telling in his own thread: the double category Rel suggests the interpretation that objects of a double category are types, arrows are terms, proarrows are predicates/relations/judgments, and cells are implications/inferences. The models of such a theory (strict or strong functors into Rel) feel "one-dimensional" in that they are like models of an algebraic theory but also allow the specification of relations and implications between those. Looking at lax functors into Span, or equivantly unitary/normal lax functors into Prof, has big consequences: it ensures that all the objects in the theory become categories and hence that models are objects of the expected two-dimensional structure. The cells of this structure are modulations, which crucially use the laxators to recover natural transformations.
This makes me wonder what kind of cells Pare is using in his double category of models. I will have to look more closely, but perhaps they are modifications between vertical and horizontal transformations? If so, you're looking at a double category of models that has different proarrows and different cells, hence is overall quite different.
Evan Patterson (Oct 11 2023 at 00:45):Evan Washington said:
I also have lots of questions, like: Do you see prospects for going in the other direction on the hierarchy of categorical logics? e.g. should there be some useful notions of double Markov categories?
Our approach seems to have good coverage of the hierarchy of categorical logic up to and including cartesian and cocartesian categories. One notable exception is that it seems not to include Markov categories. The reason is that Markov categories do something that is arguably not very categorical: they specify a not-necessarily-natural transformation, namely the family of copying operations. By contrast, in a model of double theory, all transformations are automatically natural. Now usually that's a feature, but in this case it's an obstruction! I find this mismatch quite annoying because in a different strand of my work, I have used Markov categories heavily.
As for the other direction in the hierarchy, while I have a pretty good feeling that there should be ways to extend this formalism to cover more expressive doctrines, the doctrines that people typically associate with categorical logic, I don't know for sure how to do it and my ideas are currently quite vague. So I guess we'll have to see what happens. I hoping that other people will have ideas too.
Patrick Nicodemus (Oct 11 2023 at 00:59):I have been thinking about lax functors C -> Span recently where C is a pseudo double category.
It occurred to me that lax functors into Span can be described in terms of a certain 2-categorical universal property.
I am working on writing down a proof of this theorem at the moment. Perhaps there are difficulties with the coherence conditions that I don't anticipate, so I don't assert fully that this is a definite theorem but it should be true.
Anyway.
Consider the 2-category Cat. A pseudo double category is a "bicategory internal to Cat", although apparently the term is pseudocategory, which is fine.
There's a 2-categorical slice category Cat/Set, whose objects are categories C equipped with a functor C -> Set. 1-cells are triangles that commute up to a lax natural transformation. 2-cells are natural transformations commuting with the triangles. This can be seen as a kind of 2-categorical grothendieck construction for the representable 2-presheaf Hom_{Cat}(-, Set).
Of course it is fibred over Cat by the forgetful functor.
I now claim that for a pseudocategory C in Cat, lax functors C -> Span are in one to one correspondence with lifts of the pseudocategory structure C along the forgetful functor Cat/Set -> Cat.
Moreover there is a 2-presheaf on (double categories, lax functors, horizontal natural transformations), or Pseudocat(Cat)
which sends each pseudocategory C to the category whose objects are "extensions of C to a category structure C -> Set"
and this 2-presheaf is represented by the double category of spans.
This claim is basically 2-categorical in nature and makes sense in defining the "pseudocategory of spans" internal to any 2-category, not just Cat. I posted about this in an earlier thread but I've developed my thoughts more.
Patrick Nicodemus (Oct 11 2023 at 01:01):In rigorously proving this, there are some ancillary issues I got distracted by, i.e. in proving that this is actually a 2-presheaf you start to want to work out general facts about universal algebra in a 2-category and general results about 2-fibrations like Cat/Set -> Cat. So it may take me a while to assemble the pieces. But the core interesting claim that Span has this 2-categorical universal property is not hard, I think.
Patrick Nicodemus (Oct 11 2023 at 01:07):And in some situations this reformulation may make it easier to construct and work with lax functors into Span, which is, as this page points out, https://ncatlab.org/nlab/show/double+profunctor, is the right notion of profunctor between double categories (or, specializing to the case where one category is , the right notion of presheaf on a single double category.)
This was my motivation for proving this, anyway.
Evan Patterson (Oct 11 2023 at 03:11):Patrick Nicodemus said:
I now claim that for a pseudocategory C in Cat, lax functors C -> Span are in one to one correspondence with lifts of the pseudocategory structure C along the forgetful functor Cat/Set -> Cat.
Cool! It's an appealing idea because it gives another perspective on why Span is the natural receiving object for lax double functors. (For some other justifications, have a look at Pare's paper "Yoneda theory for double categories," if you haven't already.)
FWIW, I used essentially the same idea in Section 3 of this blog post back when I was trying to figure out what the double Grothendieck construction is. I didn't get to your further ideas about a 2-presheaf on double categories, though. Interesting stuff.
Patrick Nicodemus (Oct 11 2023 at 04:14):Ah, ok. Yeah, that makes sense. The application I had in mind was that Grandis and Pare also suggest that this works well at the three dimensional level, for "intercategories", which are triple categories weak along two directions. They again define the "intercategory of sets" as the triple category Span(Span(Sets)), which made me think that some formal treatment of the construction X |-> Span(X) was needed
Patrick Nicodemus (Oct 11 2023 at 04:17):I am trying to do something possibly similar with your blog post but in 3 dimensions and for profunctors. If you think of the grothendieck construction as converting a more standard notion of presheaf C^op -> Sets nto an "internal profunctor" 1 -|-> C
Patrick Nicodemus (Oct 11 2023 at 04:19):then the grothendieck construction is giving some correspondence between these two formalisms for profunctors, I guess, though I don't fully know how to make that precise in general. I guess "Internal profunctors" can be thought of as profunctor tabulations.
Nathanael Arkor (Oct 11 2023 at 07:16):Patrick Nicodemus said:
A pseudo double category is a "bicategory internal to Cat", although apparently the term is pseudocategory, which is fine.
There's a conceptual difference between a pseudocategory and an internal bicategory: in a pseudocategory, one specifies 0-cells and 1-cells as data, but requires the category laws to hold only up to invertible 2-cell in the 2-category in which the pseudocategory is being considered. In an internal bicategory, one specifies 0-cells, 1-cells, and 2-cells as data.
Claudio Pisani (Oct 11 2023 at 20:33):In your paper you say (on page 39) that symmetric multicategories (aka colored operads) do not seem be models of any cartesian double theory.
Probably you are not aware of my paper (see also these slides), where it is shown that , the opposite of the double category of pullback squares in finite sets, is in fact such a theory.
(The double category of pullback squares in any extensive category has sums, so that its opposite is cartesian.)
The idea is that to a symmetric multicategory there corresponds a product preserving double lax functor , which
The only reason why does not fit your definition of cartesian double theory seems to me the fact that it is not small.
To set this, one can consider a skeleton of finite sets, even if this seems to me rather unnatural. Indeed I think that many of the complications in the classical theory of symmetric multicategories can be overcome by allowing families with arbitrary indexing set, that is by becoming non-skeletal.
Evan Patterson (Oct 12 2023 at 01:56):Wow, it's amazing that you can do this! I haven't yet grokked all the details but I think I get the idea. Thanks for pointing this out.
Evan Patterson (Oct 12 2023 at 02:00):Smallness of the double theory doesn't actually play a role in our paper. We just assume it because that's what's often done for theories, but this example suggests that it can also be useful to consider non-small theories.
Nathanael Arkor (Oct 12 2023 at 07:40):Evan Patterson said:
Smallness of the double theory doesn't actually play a role in our paper. We just assume it because that's what's often done for theories, but this example suggests that it can also be useful to consider non-small theories.
If your theories are not small, presumably you no longer have large double categories of models, but rather "very large" ones. In the one-dimensional setting, this would mean losing properties like local presentability. (Also, if I understand correctly, one would want to restrict to the skeleton of finite sets to recover precisely the definition of symmetric multicategory, rather than something merely equivalent to it?)
Claudio Pisani (Oct 12 2023 at 12:08):Evan Patterson said:
Wow, it's amazing that you can do this! I haven't yet grokked all the details but I think I get the idea. Thanks for pointing this out.
Thank you. I think that it fits well with your general framework, being a significant instance of cartesian double theory.
Evan Patterson (Oct 12 2023 at 16:51):Nathanael Arkor said:
If your theories are not small, presumably you no longer have large double categories of models, but rather "very large" ones. In the one-dimensional setting, this would mean losing properties like local presentability.
Yeah, that makes sense. In the paper we don't establish any properties of the double category or equipment of models beyond that it exists, but it stands to reason that certain nice double-categorical properties (whatever those might be) would then fail if the theory weren't small.
Kevin Arlin (Oct 12 2023 at 18:20):I think the question here is really just about small vs essentially small theories, of which the models are certainly going to be equivalent to an ordinary large double category. So it really shouldn't matter at all.
Evan Patterson (Oct 20 2023 at 16:46):Some bonus content following up the paper: a blog post on "retrotransformations", a third kind of morphism between models of double theories which are to cofunctors as natural transformations are to functors and modules are to profunctors.
Evan Patterson (Apr 16 2024 at 16:00):I have a new paper out on arXiv:
Among other things, it explains how to get a [[cartesian bicategory]] from a double category with finite products. This includes cartesian equipments like those of relations, span, or profunctors.
The paper is a sequel to another recent paper, which analyzes the notion of "products in a double category" mentioned above:
I think that together the two papers make a compelling case that double categories are the right setting to study the cartesian structure of "Mod-like" bicategories. Of course, I'm not the only or the first person to suggest this, but it seems that the connections between the double-categorical and bicategorical ideas involved had not previously been very well understood.
Morgan Rogers (he/him) (Apr 17 2024 at 07:19):What is the "Mod" in "Mod-like" short for?
Nathanael Arkor (Apr 17 2024 at 08:36):The bicategory of monads and bimodules in a (sufficiently locally cocomplete) bicategory K is often denoted Mod(K).
Evan Patterson (Apr 17 2024 at 18:27):Right, that was an oblique reference to the introduction to Mike Shulman's paper "Framed bicategories and monoidal bifibrations," which draws a distinction between "Cat-like" bicategories and "Mod-like" bicategories. What makes double categories so useful is that they help formalize this distinction by embedding the "Cat-like" bicategories (which are in fact 2-categories) in the "tight" direction and embedding the "Mod-like" bicategories (which are often, but not always, genuinely weak) in the "loose" direction. The two directions are then treated quite asymmetrically by the theory of double categories, which might seem odd at first but is actually entirely appropriate to the structures involved.
David Corfield (Apr 30 2024 at 11:39):Sorry if this has been addressed already, but how might someone arguing for the value of double categories respond to Antonin Delpeuch's argument in The word problem for double categories that:
free 2-categories already provide the appropriate notion of “free double category with pinwheel composites”, in the sense that they capture the desired combinatorics with a much simpler axiomatization.
We suspect that other uses of double categories, for instance in computer science..., could be recast in 2-categories without loss of expressivity, as they do not rely on the exclusion of pinwheel composites.
Nathanael Arkor (Apr 30 2024 at 12:16):To me, it appears there is an intermediate step in Delpeuch's construction of a 2-category from a double category that sheds some light on what is going on. In particular, the intuition behind the construction is given by "rotating 2-cells by 45 degrees".
image.png
There is a nice way to make this intuition precise. First, one freely adds companions to the double category. Next, one bends the horizontal wires, using the companion structure. Then, one forgets the horizontal structure, producing a 2-category.
It is clear from this perspective that Delpeuch's construction forgets some important structure: namely, which 1-cells in the induced 2-category came from horizontal arrows, and which came from vertical arrows. The distinction is important, and it would not be possible to recover certain double categorical constructions from the induced 2-category. It would be more accurate to say that "uses of double categories [...] could be recast in the language of [[F-categories]]" (but this would no longer be a simplification, because F-categories contain more structure than double categories).