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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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 Cn(x1,…,xn)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 C0(x1,x2,x3)C_0(x_1,x_2,x_3) of composable strings for the binary composition, rather than having it on all on C0(x0,x1)×C0(x1,x2).C_0(x_0,x_1)\times C_0(x_1,x_2).