Prerequisites: The Token Language for the four generators, and The Incidence Reduction for the lens that the second half of this post leans on.
Across this blog we've built Petri nets, analyzed them with ODEs, proved transitions in zero knowledge, composed them via typed links, and read strategic values through lenses — and the techniques carry from one model to the next. The structure underneath that is the symmetric monoidal category (SMC). A Petri net doesn't just get modeled by an SMC — it generates one, freely. Every net we've built, guards set aside, is a set of generators for a category where parallel composition is the monoidal product and the wiring between components respects symmetry.
A Petri net transition consumes tokens from input places and produces tokens into output places. In categorical terms, this is a morphism — a map from domain to codomain:
The transition t with inputs {p1, p2} and outputs {q1, q2, q3} is a morphism:
t : p1 ⊗ p2 → q1 ⊗ q2 ⊗ q3
The ⊗ is the monoidal product — it means "these things exist side by side." Two tokens in separate places aren't combined or merged; they coexist independently. The monoidal product is how Petri nets express concurrency: p1 ⊗ p2 means both places are marked, and both tokens are available simultaneously.
Places generate the objects; the objects themselves are multisets of places, so a marking is an object in the free commutative monoid on the places. Transitions generate the morphisms. (Keep the level straight: a single place is a generator, not the general object, and a single transition is a generator, not the general morphism. Later, when we compose whole nets along boundaries in OPetri, the nets become the morphisms — that is a different category, one level up.)
Every category has composition of morphisms. A monoidal category adds a second operation: the monoidal product. These correspond exactly to the two ways we compose Petri nets.
Sequential composition (f ; g): the output places of transition f become the input places of transition g. Tokens flow through. This is ordinary morphism composition — the same operation that makes categories useful for modeling processes with stages.
Parallel composition (f ⊗ g): two transitions sit side by side with no shared places. They fire independently. This is the monoidal product — it expresses concurrency without interaction.
The symmetry is the swap map σ : A ⊗ B → B ⊗ A. It says we can reorder the components of a parallel composition without changing the behavior. In Petri net terms: the order we list the places doesn't matter. A net with places {stock, orders} is the same net as {orders, stock}. This is exactly the commutativity property we noted in Categorical Net Types — schema order doesn't matter because the composition is symmetric monoidal.
The formal result, due to Sassone (1995) and Meseguer-Montanari (1990), is:
A Petri net generates a free symmetric monoidal category whose objects are multisets of places and whose morphisms are equivalence classes of transition firings.
"Free" means nothing extra is imposed — the only equations are the ones forced by the SMC axioms (associativity, unitality, symmetry). The category captures exactly the net's behavior and nothing more. The hypothesis matters: this is a theorem about ordinary nets, where every arc consumes or produces. Montanari and Rossi (1995) showed that nets with read arcs — contextual nets — fall outside it, which is why guards keep turning up below as the exception (two boundaries).
What this gives us:
Associativity. Composing transitions is associative: (f ; g) ; h = f ; (g ; h). We can bracket firing sequences however we want. This is why event sourcing works — the fold over events doesn't depend on how we chunk the replay.
Unit. The identity morphism on a place is "do nothing — the token stays." Every place has an identity, and composing with it changes nothing. This is why idle places don't affect analysis.
Symmetry. The swap σ : A ⊗ B → B ⊗ A is natural. Reordering places is an isomorphism, not a transformation. This is why ODE signatures are invariant under reordering: go-pflow's TestLargeScaleShuffleAnalysis shuffles the places, transitions and arcs of the tic-tac-toe model 100 times and requires the ODE trajectories to match the original's, within the solver's tolerance, every time (not re-run for this revision).
Bifunctoriality. Sequential and parallel composition interact correctly: (f₁ ⊗ f₂) ; (g₁ ⊗ g₂) = (f₁ ; g₁) ⊗ (f₂ ; g₂) when the wiring matches. In net terms: firing two independent transitions and then two more independent transitions is the same as firing each pair sequentially. This is why concurrent execution and sequential replay produce the same result.
Most of the earlier posts lean on this structure without naming it.
The Token Language defines cell, func, arrow, guard. The first three are generators of a free SMC: cells generate the objects, funcs the morphisms, and arrows give each func its domain and codomain. Guards are the exception. A guard is a predicate on the current marking — the right context R, recomputed every step — and it sits outside the free SMC rather than inside it, for the Montanari–Rossi reason above. The four-term DSL in go-pflow is a syntax for writing those generators plus that layer of predicates.
Categorical Net Types defines five specializations. Each net type is a sub-SMC with additional structure — WorkflowNet tracks a control-flow cursor (one cursor's runs are paths, closer to a free category than a free SMC), ResourceNet adds conservation (P-invariants, yᵀC = 0), GameNet combines both. The typed links (EventLink, DataLink, TokenLink, GuardLink) are what that post treats as morphisms between sealed schemas. Whether each link type preserves the structure its endpoints demand, as a functor between the sub-SMCs would have to, is not something we've checked — and a GuardLink carries a guard, which puts it on the contextual side.
Declarative Differential Models define the ODE system by reading the incidence matrix. C (places × transitions) is the linear map ℤ^T → ℤ^P sending each transition to post − pre: the free SMC's generators, abelianised. It lives on the integers rather than on the free commutative monoids, because its columns have negative entries. Reading mass-action kinetics as a functor from the discrete SMC to continuous dynamics is the natural next claim, but we haven't pinned down the target category, so for now it is a shape and not a result.
The Incidence Reduction works because the decoupled ODE system respects the monoidal product structure. Each accumulator's equation ẋᵢ = 1 - nᵢxᵢ is independent — the product decomposition of the lens mirrors the monoidal product of the SMC. No information leaks between components because the monoidal product means independence.
ZK Proofs verify transition firings — morphism validity — without revealing the marking. The Groth16 circuit encodes the incidence matrix (the SMC's morphism structure) as arithmetic constraints. The proof says "this morphism was applied to a valid object and produced a valid object" without disclosing which object. Privacy is a property of the morphism, not the objects.
ODE Signatures are invariant under isomorphism in the SMC. Two nets with different labels but the same wiring produce identical ODE solutions because isomorphic nets generate isomorphic free SMCs. The signature is a categorical invariant — it depends only on the isomorphism class, not the representation. The shuffle test above checks the reordering half of that; the ODE Signatures post describes the relabeling half, a Go struct and a pflow.xyz JSON-LD file with different place names giving the same trajectories.
The lens structure we identified in the incidence reduction has a precise SMC interpretation.
A lens in a monoidal category is a pair of morphisms — Get and Put — satisfying coherence laws. For the analysis net:
For this net the analysis lens is a tensor of per-place lenses, Lens(A ⊗ B) ≅ Lens(A) ⊗ Lens(B), and the reason is specific to it: each accumulator obeys ẋᵢ = 1 − nᵢxᵢ, and no two of those equations share a variable. That is why dynamic evaluation works — updating one position's marking doesn't touch another's lens. It is not a general fact about lenses in an SMC. Where resources are shared, as in the coffee shop, the equations couple and the ODE has to simulate rather than count.
The lens decomposition we found in the incidence reduction has a counterpart on the game-theory side: the open games of Ghani, Hedges, Winschel and Zahn (Compositional Game Theory, 2018).
In open games, a game is a lens-like gadget with a forward pass that carries players' strategies to outcomes and a backward pass that propagates utilities back to decision points. Open games are the morphisms of a symmetric monoidal category, so they compose sequentially (players move in order) and in parallel (players move independently) — the two SMC operations. The paper shows that standard games can be written this way while keeping the same Nash equilibria and off-equilibrium best responses.
Our construction has the same shape from the Petri net side. Get maps markings to strategic values; Put updates a marking and recomputes; for the analysis net the lens splits into one independent lens per place, much as independent players give independent games. The match is in shape, and it stops in specific places. Their objects are types of play, ours multisets of places, and both live in an SMC. Their morphisms are games, which carry a forward and a backward pass; our transitions don't — the backward direction lives in the analysis lens, not in the transition. Both decompositions run along ⊗, but we haven't shown they are the same theorem. Riley's Categories of Optics (2018) is the general framework in which both could be stated side by side.
The game models in this blog — tic-tac-toe, Hold'em — look like open games built from Petri net transitions: reading the ODE's fixed point plays the role of an optic's backward pass, and updating a marking and recomputing is the lens's Put. We have not written either model as an open game and compared equilibria, so "they agree" would claim more than we've checked. Tic-tac-toe is also a caution about what the backward pass computes: the fixed point counts live lines rather than searching, and mis-ranks a forced tactic until the opponent's policy is declared as structure too.
Hedges and coauthors started with games and discovered they form an SMC of optics. We started with Petri nets and discovered the analysis produces optics. I don't think that's a coincidence. Any system where independent components evaluate independently will produce this pattern, because that's what the monoidal product means.
Step back and look at what we've built across this blog. The layers compose:
Theory (objects): DDM, Token Language, Net Types, JSON-LD — these are the generating objects of the ecosystem's SMC.
Models (morphisms, in the OPetri sense — whole nets between boundaries): Tic-tac-toe, coffee shop, Hold'em, enzyme kinetics, sudoku — each is a morphism built from the theory generators.
Analysis (functors, loosely): Incidence reduction, ODE signatures, P-invariants — maps from nets to their properties.
Proofs (natural transformations, loosely): ZK proofs, lenses, sealed invariants — meant to hold uniformly across models rather than per model.
Each layer composes with the ones above and below it. Models compose via typed links. Analysis composes via functor composition. Proofs compose via vertical composition of natural transformations. The whole stack looks like an SMC of SMCs — a 2-category, if you squint. I'm describing the shape, not claiming I've checked the coherence laws, or even that each analysis map preserves ⊗.
Nobody designed the blog this way; the posts accumulated one at a time, each solving a specific problem. What the shape predicts, and what we can point to, is transfer between posts. The same ODE machinery runs on tic-tac-toe and on poker — though on poker it has to simulate rather than count. The ZK circuit that proves tic-tac-toe transitions is parameterised by topology constants rather than by the game. The EventLinks that wire order processing to inventory in the net types example are not specific to orders or inventory.
Here is what the structure buys in practice, and how much of each is actually established.
Models compose without surprises, as far as the ordinary arcs go. In the CompositeNet order example, adding EventLinks between a WorkflowNet and a ResourceNet leaves both seals — mutual exclusion, conservation — intact. A GuardLink is different: it adds a guard, a contextual arc, which is exactly where the free structure stops (two boundaries), so monotonicity there has to be argued case by case rather than read off the SMC axioms.
Analysis transfers across domains because the incidence reduction reads only C, so it runs the same way on games, resources and biochemistry whatever the tokens represent. Calling it a functor is a hope: it maps nets to values, but what composition of nets goes to on the value side is unchecked, and once resources couple, the counting shortcut fails and the ODE has to simulate.
Proofs are generic because the ZK circuit encodes the incidence matrix, not the application. Swapping topology constants gives proofs for a different game, a different workflow, a different token standard. "Natural transformation" names that uniformity by analogy; we haven't proved it is one.
The ODE keeps disjoint components independent: two nets side by side give two uncoupled ODE systems, which is the monoidal product doing its job under mass-action kinetics. The decoupling lemma is a narrower result than that. It is proved in the paper for the analysis net, where the play transitions are catalytic and each accumulator has its own drains, and it is not a theorem about monoidal functors in general.
Lenses decompose cleanly for the same reason: each place gets its own lens, composed in parallel, because the per-place equations share no variables. Dynamic evaluation updates one lens without touching the others.
For readers of the March version (revised 2026-10-01):
Lens(A ⊗ B) ≅ Lens(A) ⊗ Lens(B) is specific to the decoupled analysis net, not a general SMC fact. The open-games correspondence is a shape match; transitions have no backward pass, and no model here has been written as an open game. Points to the tic-tac-toe correction on what the fixed point computes.For the net type taxonomy: Categorical Net Types
For the lens interpretation: The Net as a Lens
For the incidence matrix as linear map: The Incidence Reduction
For the ZK circuit encoding: Zero-Knowledge Proofs for Petri Nets
For three independent analyses converging on the same boundary — the ρ boundary, inside C: Earned Compression
For settlement networks as a sub-SMC of OPetri, and for where the free structure stops (contextual arcs): The Category Settle
For what the SMC encoding loses — why flattening into morphisms erases the tense boundary between past and future: The Zipper Whose Hole Is a Universe
See also Petri Nets as a Universal Abstraction for the full treatment of these ideas.