Abstract

String diagrams are a graphical calculus for visualising and reasoning about monoidal categories in general, and 2-categories in particular. They aim to combine some of the benefits of the two standard ways of categorical reasoning: the intuitive graphical layout and type information we have in diagram chasing, and the calculational approach of equational reasoning via commutativity laws. String diagrams also simplify the expression of many categorical properties by making some coherence conditions (such as functoriality and naturality) implicit in the notation. This often results in very intuitive, visual proofs of theorems that would otherwise require complicated diagram pasting or long chains of equalities. This talk will give an introduction to string diagrams: how they are constructed and how we can read off both equational laws and commutative diagrams from a string representation. We will see how more advanced concepts such as adjunctions and monads are expressed using string diagrams, and conclude with a very clear graphical proof of how the composition of adjoint functors gives rise to a monad-comonad pair.