Title: New reasoning techniques for monoidal algebra

Aleks Kissinger

Algebraic structures in monoidal categories are best reasoned about using string diagrams and diagram rewriting. While this is a powerful tool for proving individual equalities between diagrams, the methods for defining and proving properties about whole families of diagrams are largely ad hoc, relying on human intuition to "fill in the blanks" in repeated diagrams of arbitrary size. One might hope to solve this problem by identifying a hierarchy of string diagram languages and developing induction principles for those languages whenever possible.

In this talk, I will talk about the "first rung" on this ladder, which we call "bang-box languages". These allow us to express string diagrams where certain parts are allowed to fan-out to arbitrary size. While the expressive power of these "bang-graphs" is quite poor, when combined with sound notions of bang-graph rewriting and induction, we can prove a surprisingly rich family of theorems. 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 reasoning tool Quantomatic.