Props [1]}, [2]} and their associated string diagrams, play a crucial technical role. Props are a convenient categorical structure that capture generic monoidal theories. Monoidal theories differ from equational theories in that, roughly speaking, blackin that we are able to consider more general monoidal structures other than the cartesian blackone. String diagrams are the syntax of props, and they are a bona fide syntax not far removed from traditional terms. For example, they can be recursively defined and enjoy similar properties as free objects, e.g. the principle of structural induction. The connective tissue between the classical story and string diagrams is Fox's Theorem [3]}, which states that the structure of cartesian categories can be captured by the presence of local algebraic structure: a coherent and natural commutative comonoid structure on each object. This implies several things: (i) that classical terms can be seen as particular kinds of string diagrams, (ii) that classical equational reasoning can be seen as diagrammatic reasoning on these string diagrams and (iii) that the prop induced from the monoidal theory of commutative comonoids — well-known to coincide with \(^\text{op}\) , the opposite of the prop of finite sets and functions — is the free cartesian category on one object. The correspondence goes further: as shown in [4]},
Lawvere theories are particular kinds of monoidal theories.
