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: practice: software

Topic: catlab.jl paracategories

Duncan (May 01 2026 at 15:42):

Good afternoon. I'm interested in formulating certain paracategories in Catlab, specifically variants of symmetric monoidal categories. It is unclear if there is a way to mechanise notions of (possibly) conditional definition (or at what level in the programming interface), so this is pretty tentative - any pointers or warnings?

Kris Brown (May 01 2026 at 17:58):

Hi Duncan, happy to help but would be great to understand what sorts of things you want to do with paracategories or concrete examples of them. As Catlab is embedded in Julia, there's nothing stopping you from starting by making your own data structure and methods for paracategories. The interesting challenge would be how those data and methods would interact with existing ones in Catlab (did you have a guess for what parts of Catlab you would want to connect with?). One starting pointer is that Catlab frequently uses Generalized Algebraic Theories as a notion of "interface" (allowing you to abstract away from all the various ways one might construct a paracategory, if there's a reasonable way to define a GAT for it).

Kevin Carlson (May 01 2026 at 18:26):

I do think paracategories are generalized algebraic, but in general they'll have an infinite GAT, given by objects $C_0$ and for every $n>1,$ a type $C_n(x_1,\ldots,x_n)$ of composable strings of arrows, with various partial composition operations among these types, plus identity terms. There's clearly not a finite axiomatization in general, though, and it would require some headscratching to even give a parameterization of an infinite axiomatization. The essentially algebraic axiomatization is a bit easier in this case. But for applications, you aren't going to care about paracategories that have nontrivial new information at arbitrarily long paths of composable arrows; in fact, I would guess that most paracategories have a string of arrows composable if and only if all its binary substrings are, and all higher compositions are then induced by the binary. These binary-generated paracategories would be easy to axiomatize in Catlab; you just need to explicitly introduce a domain $C_0(x_1,x_2,x_3)$ of composable strings for the binary composition, rather than having it on all on $C_0(x_0,x_1)\times C_0(x_1,x_2).$

Duncan (May 11 2026 at 15:21):

Hi Kris and Kevin, thanks for getting back to me. I will elaborate a little! I am a PhD student at the university of Glasgow.

I'm interested in implementing Milner's bigraph formalism using Catlab. These are a sort of compound hierarchical graph structure also equiped with rules for rewriting the graph. The composition of bigraphs is within symmetric monoidal (para)categories where composition and tensor product are relaxed (then similarly for symmetries). Milner calls these symmetric partial monoidal categories (SPM). Actually, Milner's (para)categories for bigraphs have bigraphs as arrows in which.

As originally formalised, it is more or less like so (to the best of my understanding):
a) The exact conditions in which arrows are defined is not part of the SPM.
b) Instead, Milner elaborates on it later. Specifically, he introduces a notion of support (in his "s-category") for an arrow, since bigraphs are arrows in an s-category, this support is a set of nodes for a bigraph structure. The condition is that these supports must be disjoint for (e.g.) composition to be defined.

So if I understand correctly, a lot of the elaboration or mechanisation of interfaces defined through @theory and @symbolic_model is Julia code. But is there much code generation?

Conversely, I might imagine for composition (in terms of code generation):
a) we would be generating a function which is partial depending on the behaviour of the paracategory
b) perhaps the behaviour is already codifiable in Catlab/Gatlab, for in Milner's s-category the condition is: check that two support sets are disjoint. That is I wondered if Catlab or GATlab view of SET might have certain machinery for this already.

John Baez (May 12 2026 at 09:08):

Paging @Evan Patterson and @Kris Brown. I am interested in bigraphs but completely unable to understand them. I hope @Duncan can figure out how to implement them in CatLab.

Evan Patterson (May 12 2026 at 22:00):

Some years ago I read a chunk of Milner's book on bigraphs. I don't remember much, but I came away with two conclusions: (1) that bigraphs are closely related to what might be called nested, undirected wiring diagrams and (2) that the formalism for bigraphs presented in that book is just not viable as mathematics: even if you can understand it, it's so baroque that you could never do anything precise with it.

That's too bad because bigraphs seem pretty interesting as a modeling language. On a more positive note, it could be a fun project to rationally reconstruct this idea with a clean formalism. Maybe someone has already done that.

Duncan, what are you interested in modeling with bigraphs?

John Baez (May 13 2026 at 08:13):

@Evan Patterson - what are nested undirected wiring diagrams?

Duncan (May 13 2026 at 09:22):

Evan Patterson said:

Duncan, what are you interested in modeling with bigraphs?

Well, I've been reading a lot about hybrid geospatial / ABM approaches. One theme is that these problems, particularly when applying statistical methods to validate the ABM somehow, are nested hierarchical (there seem to be two aspects, data collection/uncertainty, and aggregation of geography/individuals moving around). One attraction of the bigraph in this area is that it's a structural model which allows one to compose nested graphs, place them within one another, and build them up incrementally - I've seen some pretty unwieldy approaches to nested graphs in the past.

Duncan (May 13 2026 at 12:27):

Evan Patterson said:

That's too bad because bigraphs seem pretty interesting as a modeling language. On a more positive note, it could be a fun project to rationally reconstruct this idea with a clean formalism. Maybe someone has already done that.

There is a bigraph presheaf representation which avoids the paracategories (but at least at my current level I would have no idea how to translate most of this into GAT): https://marino.miculan.org/assets/pdf/UDMI012013.pdf

I've also seen another approach called gs-graphs which seem to have most of the nice compositional properties, might be more appropriate for Catlab as-is: https://dl.acm.org/doi/10.5555/2692010.2692014

Evan Patterson (May 28 2026 at 05:02):

John Baez said:

Evan Patterson - what are nested undirected wiring diagrams?

Good question :) That's what I wanted to know at the time, and I still don't know a nice formalism to think about these. Part of the issue is that different applications might actually require different notions.

IIRC, at the time, I was thinking about UWDs as a way to describe operations like conjunctive database queries or tensor contractions. To compute these efficiently, you don't want to do it all at once, but break it down into binary joins/contractions. It's natural to represent that hierarchical decomposition as a nested UWD.

Evan Patterson (May 28 2026 at 05:05):

Recently I found myself wondering about nested UWDs again. In CatColab, you can compose models (by variable sharing) in a hierarchical fashion. It would be cool to visualize a composition of arbitrary depth all at once as a kind of nested UWD. Currently you can just visualize at one level.

Evan Patterson (May 28 2026 at 05:08):

Duncan said:

Well, I've been reading a lot about hybrid geospatial / ABM approaches...

Sounds neat! Do you have a reference that includes example of this sort of model?

Evan Patterson (May 28 2026 at 05:10):

Duncan said:

I've also seen another approach called gs-graphs which seem to have most of the nice compositional properties, might be more appropriate for Catlab as-is: https://dl.acm.org/doi/10.5555/2692010.2692014

Thanks for this reference, I don't believe I've seen it.

David Corfield (May 28 2026 at 08:51):

I think the approach proposed by Sophie Raynor, I mentioned here, would allow for a form of zooming in and out of networks of networks, both directed and undirected. The $\mathbb{T}$ component of the monad $\mathbb{O}$ she discusses is all about graphs of graphs composition:

David Corfield (May 28 2026 at 09:05):

She points in that paper to the applications she expects to follow:

Finally, a word on potential applications of this work outside mathematics. My own interest in circuit algebras, modular operads, and other operadic structures governed by graphs was originally motivated by questions involving complex networks with structure at multiple scales: Given a circuit algebra $A$, the bar construction for $\mathbb{L}\mathbb{D}\mathbb{T}$ and $A$ may be viewed as a rulebook for zooming in and out of networks decorated by $A$. Indeed, there is an increasing body of work exploring this operadic (or monadic) approach in applications to fields such as systems engineering, dynamical systems, software engineering and neuroscience (see e.g., [40]). Just as they provide the main difficulty for constructing the circuit algebra monad, cycles – or “feedback loops” – are the drivers of complexity in many real world networks (see e.g., [18, 19]). The approach of this work (and [41]) highlights the combinatorial structure of loops and may therefore shed light on the properties of feedback loops as they appear in diverse applications.