Equational reasoning with lollipops, forks, cups, caps, snakes, and speedometers

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. As an alternative, we advocate the use of string diagrams, a two-dimensional form of notation which silently deals with these distracting bookkeeping steps. While originally developed to reason about functors and natural transformations, we show that string diagrams can also easily accommodate objects and arrows. Throughout the paper 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.