We give a characterization of colored Petri nets as monoidal double functors. Framing colored Petri nets in terms of category theory allows for canonical definitions of various well-known constructions on colored Petri nets. In particular, we show how morphisms of colored Petri nets may be understood as natural transformations. The displayed category construction explains how lax double functors are equivalent to functors with codomain their former domain. We use this result to characterize the unfolding of colored Petri nets in terms of free symmetric monoidal categories.

We present a unified framework for Petri nets and various variants, such as pre-nets and Kock’s whole-grain Petri nets. Our framework is based on a less well-studied notion that we call $\mathrm{\Sigma }$-nets, which allow finer control over whether tokens are treated using the collective or individual token philosophy. We describe three forms of execution semantics in which pre-nets generate strict monoidal categories, $\mathrm{\Sigma }$-nets (including whole-grain Petri nets) generate symmetric strict monoidal categories, and Petri nets generate commutative monoidal categories, all by left adjoint functors. We also construct adjunctions relating these categories of nets to each other, in particular showing that all kinds of net can be embedded in the unifying category of $\mathrm{\Sigma }$-nets, in a way that commutes coherently with their execution semantics.