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.
Matteo Capucci (he/him) (Oct 16 2022 at 00:39):[It seems this is the best place where to advertise this, so I'm gonna have to start my thread here!]
So I bit the bullet and started a curated list of material about double categories :cat::cat:, with particular focus on the recent wave of applications (it's insane how much stuff came out this year only??)
It's still very far from complete, so please contribute! (if you don't know how to use PRs, just open an issue with the stuff you'd like to see added, or DM me here)
Mike Shulman (Oct 16 2022 at 00:46):Nice! Some or all of this could also be added to the nLab [[double category]] page.
fosco (Oct 16 2022 at 07:49):@Matteo Capucci (he/him) , you lost a perfect occasion to entitle your document "Prepare for trouble, make it double"! image.png
Nathanael Arkor (Oct 16 2022 at 10:58):@Matteo Capucci (he/him): instead of adding a link to the GitHub repository on the nLab page, why not simply update the nLab page with all of the references? Creating a separate repository just means there are now two places people need to check for references instead of one.
Spencer Breiner (Oct 16 2022 at 11:58):Here is an application in robotics/hybrid systems:
https://arxiv.org/abs/1911.01267
Fabrizio Genovese (Oct 16 2022 at 14:04):Question: How do double cats behave wrt implementation? I honestly don't know and I'm curious!
Jacques Carette (Oct 16 2022 at 14:19):What do you mean by "implementation"?
Fabrizio Genovese (Oct 16 2022 at 14:22):If I have a double-categorical model of some sort, is there an established set of best practices to bring it to, say, Haskell or Rust in a performant way?
Fabrizio Genovese (Oct 16 2022 at 14:24):For instance, open games and decorated/structured cospans have been quite popular also because producing software suites relying on those formalisms has been largely feasible. So you can move from 'ideas on paper' to 'i'm running my ideas on a computer'. What I am asking is at what point we are wrt this when it comes to double categories
Fabrizio Genovese (Oct 16 2022 at 14:25):Fabrizio Genovese said:
If I have a double-categorical model of some sort, is there an established set of best practices to bring it to, say, Haskell or Rust in a performant way?
It can also be non-performant for now btw, I'm just curious to know if there's work in this direction
Jacques Carette (Oct 16 2022 at 14:36):Aha, thanks for the answer, as it wasn't the one that I expected (and would have involved Coq/Agda/Idris/Isabelle...)
Fabrizio Genovese (Oct 16 2022 at 14:46):I'm an applications guy after all lol
John Baez (Oct 16 2022 at 17:04):It's sort of a subset of Kenny's thesis, but there's this:
John Baez (Oct 16 2022 at 18:49):It's like the prequel to "Structured and decorated cospans" - it introduced double categories of structured cospans.
Max New (Oct 16 2022 at 21:29):In addition to my papers on gradual typing that Dan linked to on twitter (and here's a blog post about the first one: https://golem.ph.utexas.edu/category/2018/02/gradual_typing.html)), an earlier "PL" application of pro-arrow equipments was this paper: https://dl.acm.org/doi/abs/10.5555/2591370.2591396
Simon Willerton (Oct 17 2022 at 11:01):My ex-student Roald Koudenburg has written on various aspects of double categories. See his arXiv page.
Matteo Capucci (he/him) (Oct 17 2022 at 15:47):Thanks for everyone's suggestions!
Matteo Capucci (he/him) (Oct 17 2022 at 15:49):@Nathanael Arkor that's a good point, my rationale was that the attitudes of the two resources are different. At least I wanted to recapitulate applications of double categories more than material on double categories themselves. Of course some basic concepts are useful. It's hard to make a distinction.
Matteo Capucci (he/him) (Oct 17 2022 at 15:50):Not that I'm against merging it in the nLab, but shoving everything at the end of [[double category]] feels sub-optimal
Mike Shulman (Oct 17 2022 at 15:50):You could make a separate page on [[applications of double categories]], perhaps.
Matteo Capucci (he/him) (Oct 17 2022 at 15:50):Oh if that's a legal move, that sounds like a great synthesis
Mike Shulman (Oct 17 2022 at 15:50):Then it could also include direct links to the nLab pages about the relevant concepts, like [[structured cospans]].
Matteo Capucci (he/him) (Oct 17 2022 at 15:51):Will do asap (so maybe in a couple of days)
Matteo Capucci (he/him) (Nov 28 2023 at 10:25):I followed @John Baez's suggestions and wrote a small explainer about 'categories as monads in spans'. I started with a more ambitious post on 'actions of double categories' and then resized the scope until I got something I could write in less than a couple of hours. Well, I'm just happy I did it :)
John Baez (Nov 28 2023 at 13:42):Great! This is a very beautiful fact, I don't think I've seen anyone write a friendly explanation before.
John Baez (Nov 28 2023 at 13:43):In fact, this very trick is used to define and accomunate different flavours of categories: just take monads in a suitable bicategory.
There's no word "accomunate" in English, or at least it's very rare. I'm not quite sure what's the right replacement.
Todd Trimble (Nov 28 2023 at 14:29):"Accommodate"?
Nathaniel Virgo (Nov 28 2023 at 14:35):'unify', maybe
Damiano Mazza (Nov 28 2023 at 14:36):Yes I think "relate" or "unify" are good. "Accomunare" means something like "group together" or, literally, "make two (or more) things have something in common".
Matteo Capucci (he/him) (Nov 28 2023 at 15:23):John Baez said:
In fact, this very trick is used to define and accomunate different flavours of categories: just take monads in a suitable bicategory.
There's no word "accomunate" in English, or at least it's very rare. I'm not quite sure what's the right replacement.
Uh, thanks for spotting. @Damiano Mazza got it right, I mistranslated from Italian. There doesn't seem to be a perfect translation, I think I'll go with 'relate'.
Matteo Capucci (he/him) (Jan 04 2024 at 20:17):I should advertise my blogging here.
Today I posted a very elementary wrote up of the very basics of factorization systems in order to record the proof that an [[orthogonal factorization system]] on a category with a terminal objecto yields a reflective subcategory thereof.
Some days ago I also wrote down a proof of a fact I have known for a while but kept misremembering, namely that Tambara modules are modules, i.e. that the free Tambara module monad is a monad of free modules.
Matteo Capucci (he/him) (Jan 04 2024 at 20:18):Suggestions and corrections are welcome!