An introduction to string diagrams
Proofs in elementary category theory typically involve either the pasting together of commuting diagrams or calculational reasoning using chains of equalities. Much of the effort in these styles can be consumed with trivial administrative steps involving functoriality, naturality, and the handling of identities. These lectures introduce as an alternative so-called string diagrams, a two-dimensional form of notation which silently deals with these distracting bookkeeping steps.
String diagrams provide category theory with a different and very distinctive visual flavour. We aim to demonstrate that they are an effective tool for equational reasoning using a variety of examples evolving around monads and adjunctions. A deductive approach is followed, discovering rather than introducing categorical concepts. While originally developed to reason about functors and natural transformations, string diagrams can also easily accommodate objects and arrows. Throughout the lectures we emphasize how the topological freedom inherent in the notation can be exploited to aid the use of geometric intuition in the development of proofs. Indeed, drawing string diagrams is a bit of an art: good diagrammatic choices can make all the difference.
- R. Hinze. An introduction to string diagrams. Photos of whiteboards from the lectures at EWSCS 2016.
- Videos from the lectures.
- R. Hinze, D. Marsden. Equational reasoning with lollipops, forks, cups, caps, snakes, and speedometers. J. of Log. and Algebr. Meth. in Program., to appear. [doi link]
March 13, 2017 17:32 Europe/Helsinki (GMT +02:00)
local organizers, ewscs16(at)cs.ioc.ee
EWSCS'16 page: http://cs.ioc.ee/ewscs/2016/