I am a triangles guy.
As my friends and family know, my maths research has always been “just about triangles”. When I was in Stockholm I made friends with some people who really liked cubes and squares. Around the same time, a coauthor told me that all my simplicial work was secretly cubical. I also ended up helping to organise two online workshops on double categories. Now I work full-time at Topos, where I hear about double categories multiple times a day.
I cannot escape the squares.
DOTS stands for double operadic theory of systems, and Sophie and David Jaz recently wrote a paper on it (Libkind and Myers 2025). Their paper works through a lot of examples (and they draw a lot of diagrams…
I am a triangles guy.
As my friends and family know, my maths research has always been “just about triangles”. When I was in Stockholm I made friends with some people who really liked cubes and squares. Around the same time, a coauthor told me that all my simplicial work was secretly cubical. I also ended up helping to organise two online workshops on double categories. Now I work full-time at Topos, where I hear about double categories multiple times a day.
I cannot escape the squares.
DOTS stands for double operadic theory of systems, and Sophie and David Jaz recently wrote a paper on it (Libkind and Myers 2025). Their paper works through a lot of examples (and they draw a lot of diagrams), which I’m not going to do today. I’m also not going to attempt to summarise the whole paper here, nor am I going to be particularly detailed or careful about proving things. Instead, I just want to tie this into the work that Evan and many others have been working on surrounding double theories and their use for CatColab (Lambert and Patterson 2023; Carlson and Patterson 2025). To give some very small historical context, DOTS can be seen as a continuation of previous work on operadic composition for systems theories, such as (Libkind et al. 2021).
DOTS is DO ⦚ TS
There are two things to say before trying to explain what DOTS is.
It’s easier to explain what a DOTS is, and then say that DOTS is the study of DOTSs. This is entirely analogous to the ambiguity in the phrase “type theory”: we can define what a type theory is, and then say that type theory is the study of type theories. This means I get to write fun-to-say sentences like “Graphs is a DOTS”. 1.
DOTS should be read as a definition with an attitude all in one, split very neatly down the middle: DO ⦚ TS. That is, the definition part is (an algebra over) a double operad, and the attitude with which to interpret this definition is as a theory of systems.
So the rest of this post will be split following this idea. First we’ll look at the DO part, and then the TS part, and finally we’ll explain one way that double theories can fit into the story. But here’s the brief takeaway from all that follows:
A DOTS is the data of three 1-categories, along with instructions for how to fit them together in such a way that we can think of them as “things”, “sub-things”, and “ways to glue things along their sub-things”. Furthermore, we can really say the word “system” instead of “thing”.
This means that you can come along with your favourite systems theory — say, Petri nets, or undirected wiring diagrams with little systems of ODES inside of them, or … — and ask “do I have a DOTS?”. But just like how you might come along with your favourite category and ask “do I have a symmetric monoidal category?”, the answer might be “I can’t really tell you unless you’re a bit more specific about some of your extra structure”.
What is a DO?
The definition of an algebra over a double operad is a categorification of that of an algebra over an operad: if we take the definition of the former (that we are still yet to give) and replace every category in sight by a set then we will recover the classical definition of the latter. For now we’ll just give a definition of the DO part with seemingly arbitrary notation and conditions, but these will be explained once we look at the TS part.
Here \mathsf{Bag}(\mathcal{C}) is the category of bags of objects in \mathcal{C}, defined as the lax slice \mathsf{FinSet}\mathrm{bij}\downarrow_\mathrm{lax}\mathcal{C} of the core of finite sets over \mathcal{C}. This is essentially a categorification of the notion of multisets of objects, \mathbb{N}[\mathcal{C}]\simeq\mathbb{N}\mathcal{C}. Then an algebra over a double operad consists of
- 1-categories \mathcal{S}, \mathcal{F}, and \mathcal{A}
- a functor \partial\colon\mathcal{S}\to\mathcal{F}
- a span \mathsf{Bag}(\mathcal{F})\xleftarrow{\sigma} \mathcal{A}\xrightarrow{\tau} \mathcal{F}
- a functor c\colon\mathcal{P}\to\mathcal{S}, where \mathcal{P} is the pullback of the cospan \mathsf{Bag}(\mathcal{S})\xrightarrow{\mathsf{Bag}(\partial)}\mathsf{Bag}(\mathcal{F})\xleftarrow{\sigma}\mathcal{A}
- (some coherence data that I’m not going to describe)
such that the following diagram commutes:

What is a TS? (or: Why is a DO?)
So we’ve given a pretty unintuitive definition of an algebra over a double operad, but why? This is where the attitude comes in, by defining some terminology.
Objects in \mathcal{S} are called systems, and the morphisms are called morphisms of systems. Don’t worry too much about what the word “system” means here. Think of this as a classic nLab-style definition: a system is just an object in the category of systems.
Objects in \mathcal{F} are called interfaces; the functor \partial takes a system to its interface, which can be thought of as its “boundary”, or as the part of the system that other systems can see and interact with.
Objects in \mathcal{A} are called interactions, which take a whole bag1 of interfaces as an input and a single interface as an output and tell us what the composition should be. (This part is just like how an algebra for an operad tells me about composition.)
The functor c\colon\mathcal{P}\to\mathcal{S} is called the composition map. It takes a bag of systems and an interaction that can take their interfaces as input (i.e. the pullback \mathcal{P}) and returns a system; the diagram commuting tells us that the system it returns has precisely the interface specified by the interaction pattern.
Double theories give DOTS
Recall (Lambert and Patterson 2023) that a double theory \mathbb{T} is simply a double category “with an attitude”, where that attitude is that we should be interested in its models, i.e. (lax) double functors M\colon\mathbb{T}\to\mathbb{S}\mathsf{pan}(\mathsf{Set}).
It turns out that any double theory \mathbb{T} gives rise to a DOTS by looking at its models, in the following way:
- The three categories:
- \mathcal{S} is the category of pairs of models of \mathbb{T}
- \mathcal{F} is the category of models of \mathbb{T}
- \mathcal{A} is the category of multi-cospans in \mathcal{F}, i.e. an object is of the form (M_i \rightarrow N \leftarrow L)_{i=1,\ldots,n} for some n\in\mathbb{N}.
- The functor \partial\colon\mathcal{S}\to\mathcal{F} is given by projection onto the second component. This means that we might as well write the objects of \mathcal{S} as (M,\partial M).
- The left leg (resp. right leg) of the span \mathsf{Bag}(\mathcal{F})\leftarrow\mathcal{A}\rightarrow\mathcal{F} is given by the source map (resp. target map) of the multi-cospans.
- The functor c\colon\mathcal{P}\to\mathcal{S} is given by taking the colimit.
- Everything just works I promise.2
This is a very particular kind of DOTS, known as a colimit DOTS (because c=\operatorname{colim}).
So which for what?
Although double theories give specific examples of DOTS3, studying them in their own right is still interesting. One thing that is particularly powerful about double theories and their models is that we can cleanly peel apart “shape” and “meaning” (syntax and semantics). For example, a really nice thing about basing CatColab to on the language of models of double theories is that we get this separation: I can build a causal loop diagram, and then afterwards decide if I want to interpret the objects and arrows as defining some linear system of ODEs.4
However, DOTS lets us specify interaction patterns (and thus compositions) much more flexibly, and talk about systems that don’t “look like categories”. This is something that double theories struggle with, since the simplest double theory — the point — already has categories as its models.
References
Carlson, Kevin, and Evan Patterson. 2025. “Instances of Models of Double-Categorical Theories.” https://arxiv.org/abs/2510.08861.
Lambert, Michael, and Evan Patterson. 2023. “Cartesian Double Theories: A Double-Categorical Framework for Categorical Doctrines.” https://arxiv.org/abs/2310.05384.
Libkind, Sophie, Andrew Baas, Evan Patterson, and James Fairbanks. 2021. “Operadic Modeling of Dynamical Systems: Mathematics and Computation.” https://arxiv.org/abs/2105.12282.
Libkind, Sophie, and David Jaz Myers. 2025. “Towards a Double Operadic Theory of Systems.” https://arxiv.org/abs/2505.18329.
Footnotes
Instead of talking about bags we could just say that everything is symmetric monoidal, and that the n-ary interactions come from the monoidal structure. But bags are neat because they’re the free symmetric monoidal widget, and then we don’t have to worry about all our functors being monoidal or anything like that.↩︎ 1.
This is my attempt at a more honest “this proof is left as an exercise for the reader”. Also, I never told you what the coherences we had to check were anyway. Really, the answer is “refer to (Libkind and Myers 2025)”.↩︎ 1.
In fact, what I’ve sketched out here is just one way of many (i.e. at least two) that they can do so.↩︎ 1.
See e.g. the CatColab causal loop diagram documentation, which describes two different ODE semantics: linear and Lotka–Volterra.↩︎