5.4 PROPs and monoidal theories

Not every domain permits unrestricted copying and deletion. A Cartesian product automatically supplies diagonals \(X\to X\times X\) and terminal maps \(X\to 1\). Physical, probabilistic, quantum, resource-sensitive, and process-oriented theories often need a tensor product without those automatic operations.

A PROP is a strict symmetric monoidal category whose objects are natural numbers, with tensor on objects given by addition. It is generated under tensor by one object, so a morphism

represents an operation with \(m\) inputs and \(n\) outputs. An algebra of a PROP \(\mathbb P\) in a symmetric monoidal category \(\mathcal V\) is, subject to the usual strictness or coherence convention, a symmetric monoidal functor

Lack describes PROPs as one-sorted symmetric monoidal theories and shows how distributive laws can compose them [ Lack , 2004 ] .

Lawvere theories and PROPs are therefore neighboring doctrines, not stages of one ladder. A Lawvere theory is Cartesian and one-sorted; a PROP is symmetric monoidal and one-sorted. The choice determines which structural maps are free and which must be explicitly generated. In synthetic creativity, discovering that copying is illegal can be as important as discovering a new operation.