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: Matteo Capucci

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

https://github.com/mattecapu/awesome-double-categories

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 and Kenny Courser, Structured cospans, https://arxiv.org/abs/1911.04630

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!

Valeria de Paiva (Sep 06 2025 at 21:48):

@Matteo Capucci (he/him) has localcharts moved around a bit? I cannot read your blog post.

Matteo Capucci (he/him) (Sep 06 2025 at 23:01):

@Owen Lynch shut down the website :( I should get around moving the posts over to my own blog. There is an archive here in the meantime

Matteo Capucci (he/him) (May 17 2026 at 12:23):

It's about time I start posting here lol... Here's some recent output!

1. Me and @David Jaz Myers recently updated our preprint on 2-classifiers in 2-categories of 2-algebras, following a very helpful review. They found a mistake which brought us to substantially alter the proof strategy for the main theorem, and surrender to work with lax/pseudo T-algebras rater than strict ones (not much is lost if you can strictify the 2-classifier anyway, as it often is the case). This new proof is much nicer though, and about as long.
2. With David again, we sent Compositionality of Lyapunov functions via assume-guarantee reasoning to ACT, which got accepted. It is a proof-of-concept paper showing how assume-guarantee verification for Moore machines emerges basically for free out of the DOTS yoga, and with minimal tweaking one can extend it to (ISS) Lyapunov certificates.
3. Finally, after two years of work on quantitative logic, me and others from the pertinent ARIA collaboration are have put out some stuff about Quantitative Linear Logic (QLL) and its applications. You can read about them on my blog. I'm very excited about this work, whose primary aim is to bridge structural (meaning categorical and logical) and quantitative (meaning statistical and analytical) methods.

Comments, questions, and ideas are welcome!

V Slicer (May 21 2026 at 13:24):

Congratulations on the papers to you both, @Matteo Capucci (he/him) and @David Jaz Myers , as well as for having it accepted to ACT. I've been especially looking forward to the paper on the double category of certified systems since the first DOTS paper mentioned this area as future work, it's great to see it out:

Our approach begins with the observation that assume–guarantee reasoning is, for certain specifications, highly reminiscent of the definition of a Moore machine. A Moore machine with action set $A$ and observation set $O$ consists of a set $S$ of states together with two functions: the view $v : S \to O$ yielding an output symbol and the update $u : S \times I \to S$ transitioning the state on receiving an input. Suppose we have a predicate $\varphi(s)$ telling us which states $s \in S$ are "safe"; our aim is to prove that when starting in a safe state we remain in a safe state so long as our input $i\in I$ always satisfies its assumptions $\alpha(i)$. We also provide a guarantee $\gamma(o)$ on output symbols $o\in O$, which holds under the assumption that we are in a safe state. In total, we analyze assume–guarantee for state-safety specifications as the pair of implications

$$\begin{pmatrix} u \\[4pt] v \end{pmatrix}\vDash\begin{pmatrix} \varphi \\[4pt] \varphi \end{pmatrix}\leftrightarrows\begin{pmatrix} \alpha \\[4pt] \gamma \end{pmatrix}\iff\begin{cases}\varphi(s)\wedge \alpha(i)\;\Rightarrow\; \varphi\bigl(u(s,i)\bigr),\\[6pt]\varphi(s)\;\Rightarrow\; \gamma\bigl(v(s)\bigr)\end{cases}$$

These have almost the same form as the functions $u : S \times I \to S$ and $v : S \to O$. In fact, we can see assume–guarantee certified Moore machines (for state-safety specifications) as Moore machines in another category — this time, a category of sets equipped with a predicate, rather than just sets in the un-certified case.

That's (a part of) the DOTS yoga :relieved: That's the microcosm :relieved:

This is, if I'm not mistaken, the first paper to use DOTS since Towards a double operadic theory of systems by Sophie Libkind and David Jaz Myers introduced it. Beyond developing double categories of certified systems, it helps to get a better picture of what using DOTS looks like in a paper and how it can be introduced to readers, which is especially helpful for someone like myself who's still learning but can't help but want to enter the DOTS yoga.

A question that comes up is: Moore machines compose by setting parameters according to variables of state or what SL and DJM call the parameter setting paradigm. Is assume-guarantee reasoning possible for other paradigms of composition such as the port-plugging paradigm or the variable sharing paradigm? And is there any idea what some of the double categories of certified systems would look like for other paradigms of composition?

Matteo Capucci (he/him) (May 21 2026 at 14:01):

Thanks @V Slicer for the kind words!

Matteo Capucci (he/him) (May 21 2026 at 14:13):

V Slicer said:

Is assume-guarantee reasoning possible for other paradigms of composition such as the port-plugging paradigm or the varabiable sharing paradigm?

Indeed, one of the main points of the paper is that fibrations of algebras of systems are a natural semantics for 'compositional logic', with the latter taking a different form depending on the kind of compositionality your systems have,. Assume-guarantee reasoning seems to have the form of parameter-setting.
Now what could e.g. port-plugging look like? I have a strong feeling it will be related to regular logic and thus behavioural mereology.

Matteo Capucci (he/him) (May 21 2026 at 14:13):

If you feel like entering the DOTSverse, this might be a cool project

Matteo Capucci (he/him) (May 21 2026 at 14:14):

I'll also refer you to these old notes of mine about compositional predicate logic