Abstract

In this talk, I will discuss the interaction of two prominent tools one uses to study algebraic structures in monoidal categories: PRO Ps and string diagram rewriting. PRO Ps are small symmetric monoidal categories which totally capture a certain algebraic structure (they are the “walking X”), but their application is typically limited to structures that we understand well. On the other hand, rewriting with string diagrams allows one to immediately get a handle on even those structures which have very complicated presentations, but it provides little in the way of powerful “meta-rules” describing the global behaviour of the structure.

To bridge this gap, one needs to find more sophisticated ways of expressing and reasoning about infinite families of diagrams. In this talk, I will introduce ”!-box notation”, which gives a particularly simple means of doing just that. While the expressive power of !-boxes is fairly limited, when combined with the notions of !-graph rewriting and induction, one can state and prove a surprisingly rich family of theorems, and sometimes even recapture the kind of global behaviour we would expect from a PROP -based approach. I will illustrate this by giving a purely graphical proof of a recent representation theorem for interacting bialgebras, and show this theorem in action in the graphical proof assistant Quantomatic.