  Whereas string diagrams for strict monoidal categories are well understood,
and have found application in several fields of Computer Science, graphical
formalisms for non-strict monoidal categories are far less studied. In this
paper, we provide a presentation by generators and relations of string diagrams
for non-strict monoidal categories, and show how this construction can handle
applications in domains such as digital circuits and programming languages. We
prove the correctness of our construction, which yields a novel proof of Mac
Lane's strictness theorem. This in turn leads to an elementary graphical proof
of Mac Lane's coherence theorem, and in particular allows for the inductive
construction of the canonical isomorphisms in a monoidal category.
