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.

§ INTRODUCTION

String diagrams are a rigorous graphical notation for category theory that is proving useful in a broad variety of application domains, such as quantum systems [5], computational linguistics [4], digital circuits [8], or signal flow analysis [3].
What the majority of string diagrammatic notations have in common is that they are devised for monoidal categories in which the tensor is strict, i.e. the associator and unitor morphisms are identities.
As Joyal and Street explain in their seminal Geometry of Tensor Calculus [11], the choice of using a strict monoidal category was motivated by convenience (“simplicity of exposition”) and by a wish to focus on “aspects other than the associativity of tensor product”.
Furthermore, they believed that “most results obtained with the hypothesis that a tensor category is strict can be reformulated and proved without this condition.”

Indeed, in terms of mathematical power, this statement is true.
However, string diagrams have been used increasingly as a convenient syntax for languages with models in (strict) monoidal categories.
And, when used as syntax, the distinction between strict and non-strict tensor becomes relevant, if not in terms of mathematical expressiveness then at least as a mechanism of abstraction.
This is why modern programming languages, and even some modern hardware design languages such SystemVerilog [16], use non-strict features such as tuples and structs which can nest in non-trivial ways.
These non-strict structures could be manually `strictified' by the programmer by flattening them into arrays.
Using such programmer conventions instead of native syntactic support does not entail a loss of expressiveness, but a loss of code readability, convenience, and general programmer effectiveness.

In this paper, we address the problem of expanding the graphical language of string diagrams with the required features that allow the expression of non-strict tensors.
What makes the language of strict tensors convenient for the graphical representation is that objects are naturally represented as lists of wires.
This suggests that string diagrams make use of strictness in an essential way and, indeed, naive attempts to define string diagram languages for non-strict monoidal categories can render the notation so heavy-going as to lose the intuitiveness that makes it so attractive in the first place.
A more sophisticated solution, which we propose here, is to deliberately use the strictification of a possibly non-strict monoidal category in order to make string diagrams function in this setting with a minimum of additional overhead.
These points will be illustrated with examples in Section <ref>.

Concretely, the basic idea is to use new operations to `pack' pairs of wires into single wires with internal tensorial structure and to `unpack' structured wires into pairs of wires labelled with the tensor component objects.
The repeated application of unpacking can flatten any wire with an arbitrarily complex tensor structure into a list of wires labelled with elementary objects.
Other new operations are used to `hide' or `reveal' wires labelled with the tensor unit.
These four families of new operations are used to define the associators and the unitors of the strictified category.

Some similar ideas are introduced in the diagrammatic calculus of weakly
distributive categories [2].
This is a significantly more complex set-up than ours, involving two distinct
tensor products and an additional kind of wire (the `thinning links').
The similarities nevertheless suggest that our construction may be recoverable
from theirs by restricting to the single-tensor case–we leave this to future
Our focus here is instead to show how the `standard' string diagrammatic syntax
for strict monoidal categories can be straightforwardly extended to support the
non-strict setting.
A key motivation for this is so that computer representations of strict string
diagrams such as [17] can be extended to include the non-strict
case essentially for free.

We propose a strictification construction yielding a graphical language for
non-strict monoidal categories. With respect to traditional string diagrams, it
provides a more fine-grained representation of tensoring, whose usefulness we
demonstrate in motivating examples drawn from circuit theory and programming
language semantics.
The bulk of the paper is then dedicated to showing that the construction is correct, i.e. the strictified category in which string diagrams live is monoidally equivalent to the original non-strict category.
Our proof of monoidal equivalence is new: in contrast to Mac Lane's we do not
rely on the coherence theorem, and instead construct the functors of the equivalence
Consequently, we are able to give a new elementary proof of the coherence
theorem: we show graphically that the free monoidal category on a single
generator forms a preorder.
The remainder of the coherence result is largely a reformulation Mac Lane's
original corollary, but in a way that we believe has pedagogical value.
We further identify and highlight some common misconceptions about this theorem, which is sometimes misunderstood as being more powerful than it really is.

In Section <ref> we present our graphical calculus
for (non-strict) monoidal categories, in the form of a strictification
Subsections <ref>, <ref>, and
<ref> illustrates a series of motivating examples.
Section <ref> justifies our construction by proving that it
yields an equivalence of categories.
Section <ref> revisits MacLane's Coherence theorem and some of
its consequences in light of the approach we presented.
Section <ref> is dedicated to conclusions and future work.

§ A GRAPHICAL LANGUAGE FOR (NON-STRICT) MONOIDAL CATEGORIES

We assume familiarity with string diagrams for strict monoidal categories, see e.g. [15]. Let us fix an arbitrary (non-strict) monoidal category $\CatC$. We construct its strictification as the strict monoidal category $\CatD$ defined as follows.

$(\CatD, \TensorD)$ is the strict monoidal category freely generated by:

* Objects $\ObjD{A}$ for each $A \in \CatC$

* Generators (<ref>), with $\MorD{f} : \ObjD{A} \to \ObjD{B}$ for each $f : A \to B \in \CatC$

* functoriality equations (<ref>)

* adapter equations (<ref>), and

* associator/unitor equations (<ref>)

Note that because $\CatD$ is strict by definition, we are entitled to use string
diagrammatic notation.

\begin{equation}
\label{equation:catd-generators}
\begin{gathered}
\tikzfig{generator-Adapter} \qquad \tikzfig{generator-AdapterInv} \\
\tikzfig{generator-adapter} \qquad \qquad \tikzfig{generator-adapterInv} \\
\tikzfig{generator-strictf}
\end{gathered}
\end{equation}

\begin{equation}
\label{equation:catd-functor-equations}
\begin{gathered}
\begin{aligned}
\tikzfig{equation-identity-lhs}    \quad & = \quad \tikzfig{equation-identity-rhs} \\
\tikzfig{equation-composition-lhs} \quad & = \quad \tikzfig{equation-composition-rhs}
\end{aligned}
\end{gathered}
\end{equation}

\begin{gather}
\label{equation:catd-adapter-equations}
\begin{aligned}
\tikzfig{equation-Adapter-naturality-1-lhs} \quad & = \quad \tikzfig{equation-Adapter-naturality-1-rhs}
\\
\tikzfig{equation-Adapter-naturality-2-lhs} \quad & = \quad \tikzfig{equation-Adapter-naturality-2-rhs}
\\
\tikzfig{equation-adapter-isomorphism-1-lhs} \quad & = \quad \tikzfig{empty}
\\
\tikzfig{equation-adapter-isomorphism-2-lhs} \quad & = \quad \tikzfig{equation-adapter-isomorphism-2-rhs}
% \tikzfig{equation-adapter-isomorphism-2-rhs}
\end{aligned}
\end{gather}

\begin{gather}
\label{equation:catd-monoidal-equations}
\begin{aligned}
\MorD{\assoc}    \quad & = \quad \tikzfig{equation-associator-rhs} \\
\MorD{\assocInv} \quad & = \quad \tikzfig{equation-associatorInv-rhs} \\
\MorD{\unitl}    \quad & = \quad \tikzfig{equation-unitl-rhs} \\
\MorD{\unitlInv} \quad & = \quad \tikzfig{equation-unitlInv-rhs} \\
\MorD{\unitr}    \quad & = \quad \tikzfig{equation-unitr-rhs} \\
\MorD{\unitrInv} \quad & = \quad \tikzfig{equation-unitrInv-rhs}
\end{aligned}
\end{gather}

This is a functorial construction, yielding a monoidal equivalence between
$\CatC$ and $\CatD$, as we will prove in Section <ref>.
Note that although the category $\CatD$ is essentially the same as that given by
Mac Lane <cit.>, its construction differs in one key respect.
Namely, to define his equivalent strict category, Mac Lane relies on the
coherence theorem to define both composition of arrows and to ensure the
functors in the equivalence are monoidal.
In contrast, the adapter generators and equations of $\CatD$ mean that
Definition <ref> does not require use of the coherence theorem,
and can therefore be used to prove it.

The functoriality equations are so-called as they ensure functoriality of the
construction. The `adapter' equations and `associator/unitor' equations further
ensure this functor is monoidal and it forms one half of a
monoidal equivalence.
Sec. <ref> will make it clear that these equations
are essentially obtained by freely adding the morphisms required by the
definition of a monoidal functor (<ref>).

Besides its mathematical significance, the interest of this construction lies in
providing a means of manipulating morphisms of non-strict monoidal categories
In particular, the $\adapter$ and $\adapterInv$ generators can be used to
explicitly summon and dispell the monoidal unit, while the $\Adapter$ and
$\AdapterInv$ generators can be thought of as systematic ways of packing and
unpacking wires into more complex wires with internal structure.
The next subsections will showcase how this additional layer of structure can be
useful in categorical models of computation.

§.§ Circuit Description Languages with Tuples

Categorical models of circuit description languages are a prime source of examples of monoidal categories, for instance combinational [12] or sequential [8] circuits.
The graphical representation of circuits also fits naturally and intuitively the box-and-wire model used by string diagrams.
More precisely, the circuit description languages in loc. cit. (and variations thereof) are instances of strict monoidal categories.

From the point of view of expressiveness, i.e. realising circuits with certain desired behaviours, the strict setting does not introduce any limitations.
Consistent with this observation, standard hardware description languages (HDL) such as Verilog can also be modelled using a strict monoidal tensor.
However, larger and more complex designs stand to benefit from the additional level of structure which a non-strict tensor can offer and, indeed, more modern HDLs, intended for more complex designs, such as SystemVerilog have syntactic facilities which require a non-strict tensor: structs.

Consider the following simple example.
Suppose that some circuitry is needed to process network packets, which consist of a header (of size $h=96$ bits), a payload (of size $p=896$ bits) and an error-correcting trailer (of size $e=32$ bits).
In the older Verilog language, the header and the payload can be combined in a single, wider, data bus of $h+p=992$ bits, but the two components can only be extracted using numerical indexing.
This is a primitive form of `flattening' a data structure into an array, and in the more modern SystemVerilog it can be avoided by using a struct.
This means that a data type of `message' (say $m$) can access its components as fields (projections), namely $m.h$ and $m.p$.
Since structs can have other structs as fields the way in which the components are associated is relevant, which means that the tensor must no longer be strict.

On the other hand, `flattening' the structure of a data bus to an array of bits can be useful.
In the current example, in computing the error-correcting code $e$, the way the message is partitioned into header and payload is no longer relevant, so it is convenient to unpack the tensor $h\otimes p$ into a flat array of $h+p$ wires from which an error-correcting code $e$ is computed by a generic circuit of the appropriate width.
Structures that can be flattened like this are called in SystemVerilog packed structs, and to model them properly both strict and non-strict tensorial facilities are required in the categorical model.

Finally, the error-correcting code can be packed with the original message into an error-correcting message with three components.
It is obviously important to be able to retrieve the header, payload, and error-correcting code separately from the message, and it should be equally obvious that once the internal structure of the message is non-trivial a calculus of indices would be a complicated, awkward, and error-prone way to access the components.

Graphically, this circuit is represented as

In order to make this diagram completely formal, what we are using here is the $\CatD$ construction described in Sec. <ref> applied to one of the categories $\CatC$ of digital circuits (combinational or sequential) mentioned earlier.
This gives us the best of both worlds: the `non-strictness' of
circuits-with-tuples, and the graphical syntax of string diagrams.

Strictifying Strict Categories

The `strictification' procedure is not just useful for
providing a graphical syntax for non-strict monoidal categories, but can also
provide a more ergonomic syntax for monoidal categories that are already strict.
Suppose we wish to work in Lafont's strict monoidal category of
circuits[12], and suppose we would like to define the `parity'
function used earlier.
Using our construction, we can define it recursively as follows:

\begin{align*}
\mathsf{parity}_0 & = \tikzfig{case-study-recursive-definition-parity-basecase} \\
\mathsf{parity}_n & = \tikzfig{case-study-recursive-definition-parity}
\end{align*}

Notice that in the `base' language of Lafont's PROP of circuits we cannot truly
depict this diagram, since there is no way to treat a bundle of $n$ wires as a
pair of $1$ and $n - 1$ wires.
To do this formally we require the adapter morphisms as defined in Section

§.§ Programming Languages

Programming languages, largely based on the lambda calculus, commonly include product formation as a syntactic feature.
Therefore, a graphical syntax based on its categorical model, as used for example in [1], needs to have a non-strict tensor.
However, having only the non-strict tensor leads to an awkward graphical syntax in which all generators have a single wire going in and a single wire going out.
Diagrams in which the interfaces can be intermediated using lists of wires require mechanisms for strictification.
This can be realised by applying the strictification construction to a Cartesian closed category, which will allow the expression of examples such as the one below.

Consider the simple task of summing two complex numbers,
whose real and imaginary parts are encoded as floating-point numbers.

That is, while we have a primitive type of reals, we model complex numbers as
pairs $\Complex = \Real \times \Real$.
A natural way to write such a program in a diagrammatic form is as follows:

\[ \tikzfig{case-study-stlc} \]

Even in categorical models of of the simply-typed $\lambda$-calculus (STLC) without product, strictification has a role to play.
As usual, this role is cloaked in informality which in some contexts can lead to ambiguity.
STLC is interpreting by giving meaning to type judgements $\Gamma\vdash t:T$ with $\Gamma$ a context, $t$ a term, and $T$ a type.
The contxt $\Gamma=x_1:T_1,\ldots,x_n:T_n$ is a list of typed variables which is interpreted as the tensor $T_1\otimes\cdots T_n$, virtually always treated as if it were strict.
This informal strictification can be problematic though with product types are used, as the objects $T_i$ in the interpretation of the context also contain tensors.
So the strictification must be fined-grained enough to allow only the flattening of those tensor representing the comma of the context, and not those of the product formation.
Our approach offers this level of granularity.

§.§ Strict vs. Non-Strict String Diagrams

Our final example concerns the usability problems of non-strict diagrams without strictification and illustrate how our approach to strictification with packing and unpacking wires makes rigorous the intuition that formulating certain properties in terms of strict monoidal categories does not entail a loss of generality.
Consider the property of braided monoidal categories to be autonomous if and only if they are right-autonomous <cit.>.
The proof is formulated in terms of string diagrams in <cit.>, which makes it more intuitive.
In a braided autonomous category each object $A$ has a dual $A^*$, there exists a family of isomorphism $c_{A,B}:A\otimes B\to B\otimes A$ called braidings, and families of adjunctions $\eta_A:I\to A^*\otimes A$, $\epsilon:A\otimes A^*\to I$ with certain properties which we may elide in the formulation of the example.

The idea of the proof is to show that isomorphisms $b_A:A^{**}\to A$, $b_A^{-1}:A \to A^{**}$ can be constructed. They are defined as follows:

\begin{align*}
& b_A = A^{**} \xrightarrow{\eta_A\otimes \id}A^*{\otimes} A{\otimes} A^{**}
\xrightarrow{\id\otimes c_{A,A^{**}}} A^*{\otimes} A^{**}{\otimes} A
\xrightarrow{\epsilon_{A^*}\otimes \id}A\\
& b_A^{-1} = A \xrightarrow{\id\otimes\eta_{A^*}}A{\otimes} A^{**}{\otimes} A^*
\xrightarrow{c^{-1}_{A^{**}, A}} A^{**}{\otimes} A{\otimes} A^*
\xrightarrow{\id\otimes\epsilon_{A}}A^{**}.
\end{align*}

The fact that $b_A;b_A^{-1}=\id$ becomes elegantly obvious when the terms are rendered as string diagrams which can be manipulated graphically:

\[ \tikzfig{motivating-examples-lemma-1} \]

The exposition includes the standard caveat that “Here we have written, without loss of generality, as if [the category] were strict monoidal.”
We shall now show, graphically, that this is indeed the case.

First we note that in the non-strict setting (without strictification) all string diagrams must be equipped with gadgets that make sure that there is a single wire on the left, and a single wire on the right.
These gadgets are of course the bundlers and unbundlers introduced earlier.
Therefore, in the non-strict setting, taking into account all the relevant associators, the diagram for $b_A$ becomes much more complicated, denying the intuitiveness we expect from a graphical notation:

\[
\scalebox{.7}{
\input{figures/lemma2.pdf_tex}
\]

This is why a naive approach to non-strict string diagram construction is not effective.
However, the complications are only an artefact of the construction of the diagram in a purely non-strict setting.
The strictification equations come to rescue and, in this case, cancel out all
bundler-unbundler pairs in the order indicated by the numerical labels attached
to them, resulting in exactly the same diagram of $b_A$ that was constructed in
the strict setting.
So, indeed, working in the strict setting implied no loss of generality!

§ STRICTNESS

We now show that $\CatC$ is monoidally equivalent to $\CatD$, constituting a
proof of Mac Lane's strictness theorem, since $\CatC$ is an arbitrary monoidal

Our approach is to define monoidal functors $\FunF : \CatC \to \CatD : \FunG$,
and we begin by recalling the definition of monoidal functor.

Monoidal Functor

Let $(\cat{C}, \otimes, \unit_\cat{C})$
and $(\cat{D}, \bullet, \unit_\cat{D})$
be monoidal categories.
A monoidal functor is a functor $F : \cat{C} \to \cat{D}$
equipped with natural isomorphisms

\[ \Adapter_{X,Y} : F(X) \bullet F(Y) \to F(X \otimes Y) \]

\[ \phi : \unit_\cat{D} \to F(\unit_\cat{C}) \]

such that the following diagrams commute for all objects $A, B, C \in \cat{C}$.

monoidal-hexagon0.9Monoidal Functor associator axiom
monoidal-squares0.8Monoidal Functor unitor axioms

With this definition it is straightforward to see how to define a
monoidal functor from $\CatC$ to $\CatD$.

Let $\FunF : \CatC \to \CatD$ be the strictification functor
defined on objects as:

\[ \FunF(A) \defeq{} \ObjD{A} \]

And on morphisms as:

\[ \FunF(f) \defeq{} \MorD{f} \]

$(\FunF, \Adapter, \adapter)$ is a monoidal functor

$\FunF$ preserves identities and composition (and is therefore a functor) by
the functor equations (<ref>):

\[ \FunF(\id_A) = \MorD{\id_A} = \id_{\ObjD{A}} \]

\[ \FunF(f \cp g) = \MorD{f \cp g} = \MorD{f} \cp \MorD{g} = \FunF(f) \cp \FunF(g) \]

It is a monoidal functor using the adapter generators
$\Adapter = \generator{g-Adapter}$ and
$\adapter = \generator{g-adapter}$
from (<ref>).
For this to work, we must have that $\generator{g-Adapter}$ is a natural isomorphism
and $\generator{g-adapter}$ an isomorphism, respectively.
This is precisely what the adapter equations
(<ref>) state.

Similarly, we require that the diagrams of (<ref>)
and (<ref>) commute.
Again, this is precisely what the the associator/unitor equations
(<ref>) state, and so $\FunF$ is a monoidal

Notice that $\CatD$ is defined by freely adding the requirements of
Definition <ref>.
Generators $\generator{g-Adapter}$ and $\generator{g-adapter}$ and equations
(<ref>) give the natural isomorphism
$\Adapter$ and isomorphism $\adapter$,
while the commuting diagrams (<ref>) and
(<ref>) are precisely the
`associator/unitor' equations (<ref>).

We can now define the other half of the monoidal equivalence $\FunF \dashv
\FunG$.

In doing so, we'll make use of the fact that morphisms of a monoidal category
can be written in a `sequential normal form'
(Appendix <ref>), i.e. as a series of `slices':

\[ (\id \otimes g_1 \otimes \id) \cp (\id \otimes g_2 \otimes \id) \cp \ldots \cp (\id \otimes g_n \otimes \id) \]

We take advantage of this form to define $\FunG$: our definition is defined on
`slices' $\id_X \TensorD q \TensorD \id_Y$ for some generator $q$,
and then freely on composition so that $\FunG(f \cp g) = \FunG(f) \cp \FunG(g)$.

We define the nonstrictification functor

$\FunG : \CatD \to \CatC$ inductively on objects:

\begin{align*}
\FunG(\unitD)              & \defeq \unitC \\
\FunG(\ObjD{A})            & \defeq A \\
\FunG(\ObjD{A} \TensorD R) & \defeq A \TensorC \FunG(R)
\end{align*}

And on morphisms we give a recursive definition, with the following base cases:

\begin{align*}
\FunG(\id_{\unitD})                       & \defeq \id_{\unitC} \\
\FunG(\MorD{f})                           & \defeq f \\
\FunG(\Adapter_{A,B})                     & \defeq \id_{A,B}    = \FunG(\AdapterInv_{A,B}) \\
\FunG(\adapter)                           & \defeq \id_{\unitC} = \FunG(\adapterInv)  \\
% q * id_Y
\FunG(\MorD{f} \TensorD \id_Y)            & \defeq f \TensorC \id_{\FunG(Y)} \\
\FunG(\Adapter_{A,B} \TensorD \id_Y)      & \defeq \assoc_{A,B, \FunG(Y)} \\
\FunG(\AdapterInv_{A,B} \TensorD \id_Y)   & \defeq \assocInv_{A,B, \FunG(Y)} \\
\FunG(\adapter \TensorD \id_Y)            & \defeq \unitlInv_{\FunG(Y)} \\
\FunG(\adapterInv \TensorD \id_Y)         & \defeq  \unitl_{\FunG(Y)} \\
% id * q
\FunG(\id_{\ObjD{A}} \TensorD \MorD{f})           & \defeq \id_A \TensorC f \\
\FunG(\id_{\ObjD{A}} \TensorD \Adapter_{B,C})     & \defeq \id_A \TensorC (\id_B \TensorC \id_C) \\
\FunG(\id_{\ObjD{A}} \TensorD \AdapterInv_{B,C} ) & \defeq \id_A \TensorC (\id_B \TensorC \id_C) \\
\FunG(\id_{\ObjD{A}} \TensorD \adapter)           & \defeq \unitrInv_{A} \\
\FunG(\id_{\ObjD{A}} \TensorD \adapterInv)        & \defeq \unitr_{A}
\end{align*}

With a single recursive case, for
$q \in \{ \Adapter, \adapter, \AdapterInv, \adapterInv, \id_{\ObjD{Q}} \}$

\begin{align*}
\FunG(\id_{\ObjD{A}} \TensorD q \TensorD r) \defeq \id_A \TensorC \FunG(q \TensorD r)
\end{align*}

Finally take $\FunG(f \cp g) \defeq \FunG(f) \cp \FunG(g)$.

This definition is well defined with respect to the equations of Definition
we give a proof in Appendix <ref>.

The definition of $\FunG$ can be explained more intuitively in terms of
If we think of each `slice' of the sequential normal form as a list of
primitive arrows of $\CatC$,
then the definition of $\FunG$ is essentially a list recursion in which
we have a separate case for $1$, $2$, and $n$-element lists.

Now we will show that $\FunG$ is a monoidal functor.
To do this, we must specify the `coherence maps': a natural isomorphism

\[ \Psi_{X,Y} : \FunG(X) \TensorC \FunG(Y) \to \FunG(X \TensorD Y) \]

and isomorphism

\[ \psi : \unitC \to \FunG(\unitD) \]

as mandated by Definition <ref>.

We define $\Psi$, the coherence natural isomorphism for $\FunG$, in the following cases:

\begin{align*}
%& : \FunG(X) \TensorC \FunG(Y) \to \FunG(X \TensorD Y) \\
\Psi_{\unitD, \unitD}
%& : \FunG(\unitD) \TensorC \FunG(\unitD) \to \FunG(\unitD \TensorD \unitD) \\
%& : \unitC \TensorC \unitC \to \unitC \\
& \defeq \unitl_{\unitC} = \unitr_{\unitC}  \\
\Psi_{X, \unitD}
%& : \FunG(X) \TensorC \FunG(\unitD) \to \FunG(X \TensorD \unitD) \\
%& : \FunG(X) \TensorC \unitC \to \FunG(Y) \\
& \defeq \unitr_{\FunG(X)} \\
\Psi_{\unitD, Y}
%& : \FunG(\unitD) \TensorC \FunG(Y) \to \FunG(\unitD \TensorD Y) \\
%& : \unitC \TensorC \FunG(Y) \to \FunG(Y) \\
& \defeq \unitl_{\FunG(Y)} \\
\Psi_{\ObjD{A}, Y}
%& : \FunG(\ObjD{A}) \TensorC \FunG(Y) \to \FunG(\ObjD{A} \TensorD Y) \\
%& : A \TensorC \FunG(Y) \to A \TensorC \FunG(Y) \\
& \defeq \id_{A \TensorC \FunG(Y)} \\
\Psi_{\ObjD{A} \TensorD X, Y}
%& : \FunG(\ObjD{A} \TensorD X) \TensorC \FunG(Y) \to \FunG(\ObjD{A} \TensorD X \TensorD Y) \\
%& : (A \TensorC \FunG(X)) \TensorC \FunG(Y) \to A \TensorC \FunG(X \TensorD Y) \\
& \defeq \assocInv_{A, \FunG(X), \FunG(Y)} \cp (\id_{A} \TensorC \Psi_{X, Y})
\end{align*}

The coherence isomorphism $\psi$ for $\FunG$ is defined as follows:

\begin{align*}
%& : \unitC \to \FunG(\unitD)
\psi_{\unitC}
%& : \unitC \to \FunG(\unitD) \\
%& : \unitC \to \unitC \\
& \defeq \id_{\unitC}
\end{align*}

Note that both $\unitl_{\unitC}$ and $\unitr_{\unitC}$ have the correct type
as a choice for $\Psi_{\unitD, \unitD}$.
In fact, they are equal: unitors coincide at the unit object, i.e.
$\unitl_{\unitC} = \unitr_{\unitC}$, as noted in

$(\FunG, \Psi, \psi)$ is a monoidal functor

It is clear that $\Psi$ and $\psi$ are natural isomorphisms since they are
both composites of natural isomorphisms.
Thus it remains to check the diagrams of Definition
<ref> commute.

The squares (<ref>) commute because $\psi = \id$,
and $\Psi_{A,\unitD} = \unitr$
and $\Psi_{\unitD,B} = \unitl$
by definition.

Now let us check that the hexagon (<ref>) commutes.
Note that in the following we use that $\FunG(\assocD) = \id$, because $\CatD$
is strict, and so the hexagon axiom becomes a pentagon.

We will approach the problem inductively, checking base cases where
$A = \unit$ and $A = \ObjD{A}$, and finally the inductive step with
$A = \ObjD{A} \TensorD R$.
Let us begin with $A = \unit$, and taking the outer path of the hexagon we calculate as follows:

\begin{align*}
& (\id_{\unitC} \TensorC \Psi_{B,C})
\cp \Psi_{\unitC, B \TensorD C}
\cp \Psi^{-1}_{B,C}
\cp (\Psi_{\unitC, B} \TensorC \id_{\FunG(C)})^{-1} \\
& = (\id_{\unitC} \TensorC \Psi_{B,C})
\cp \unitl_{\FunG(B \TensorD C)}
\cp \Psi^{-1}_{B,C}
\cp (\unitl_{\FunG(B)} \TensorC \id_{\FunG(C)})^{-1} \\
& = \unitl_{\FunG(B) \TensorC \FunG(C)}
\cp (\unitl_{\FunG(B)} \TensorC \id_{\FunG(C)})^{-1} \\
& = \assoc_{\unitC, \FunG(B), \FunG(C)}
\end{align*}

Wherein we expanded the definition of $\Psi$, then used naturality of $\Psi_{B,C}$
before applying the monoidal triangle lemma of <cit.>.

Now consider the second base case, where $A$ is the `singleton list' $\ObjD{A}$.
In this case, the hexagon diagram commutes immediately
because $\Psi_{\ObjD{A},B} = \id_{\ObjD{A} \TensorC \FunG(B)}$
and $\Psi_{\ObjD{A}, B \TensorD C} = \id_{\ObjD{A} \TensorC \FunG(B \TensorD C)}$.
More explicitly, we calculate as follows, starting again with the outer path
of the hexagon and expanding definitions:

\begin{align*}
& (\id_A \TensorC \Psi_{B,C})
\cp \Psi_{A, B \TensorD C}
\cp \Psi^{-1}_{A \TensorD B, C}
\cp (\Psi_{\ObjD{A},B} \TensorC \id_{\FunG(C)}) \\
% This step is too wide to typeset...
%    & = (\id_A \TensorC \Psi_{B,C})
%      \cp \id_{A \TensorC \FunG(B \TensorD C)}
%      \cp (\assocInv_{A, \FunG(B), \FunG(C)} \cp (\id_A \TensorC \Psi_{B,C}))^{-1}
%      \cp (\id_{A \TensorC \FunG(B)} \TensorC \id_{\FunG(C)}) \\
& = (\id_A \TensorC \Psi_{B,C})
\cp (\id_A \TensorC \Psi_{B,C})^{-1}
\cp \assoc_{A, \FunG(B), \FunG(C)} \\
& = \assoc_{A, \FunG(B), \FunG(C)}
\end{align*}

Finally let us prove the inductive step.
Assume that the hexagon commutes for objects $R$, $B$, $C$, giving us the

\begin{align*}
\Psi_{R, B \TensorD C} & \cp \Psi^{-1}_{R \TensorD B, C} \\
& = (\id_{\FunG(R)} \TensorC \Psi^{-1}_{B,C})
\cp \assoc_{\FunG(R), \FunG(B), \FunG(C)}
\cp (\Psi_{R,B} \TensorC \id_{\FunG(C)})
\end{align*}

We may then rewrite the following subterm of the monoidal hexagon as follows:

\begin{align*}
\id_A & \TensorC (\Psi_{R, B \TensorD C} \cp \Psi^{-1}_{R \TensorD B, C}) \\
& =   \id_A \TensorC (\id_{\FunG(R)} \TensorC \Psi^{-1}_{B,C}) \\
& \cp \id_A \TensorC \assoc_{\FunG(R), \FunG(B), \FunG(C)} \\
& \cp \id_A \TensorC (\Psi_{R,B} \TensorC \id_{\FunG(C)})
\end{align*}

We can then rewrite
$\id_A \TensorC \assoc_{\FunG(R), \FunG(B) \FunG(C)}$
using the monoidal category pentagon axiom,
and then use naturality of $\assoc$ to reduce the outer path of the
monoidal hexagon until we are left with
$\assoc_{A \TensorC \FunG(R), \FunG(B), \FunG(C)}$,
as required.

Finally, we must check that $\FunF$ and $\FunG$ indeed form an equivalence.

First, recall the definition

Equivalence of Categories

An equivalence is a pair of functors

\[ \cat{C} {\overset{F}{\rightarrow} \atop \underset{G}{\leftarrow}} \cat{D} \]

and a pair of natural isomorphisms

\[ \eta : \id_{\cat{C}} \to G \circ F \]

\[ \epsilon : F \circ G \to \id_{\cat{D}} \]

Explicitly, we require the following two diagrams to commute:

\begin{equation}
\scalebox{0.9}{\input{tikz/equivalence-naturality-eta.tikz}}
\qquad
\scalebox{0.9}{\input{tikz/equivalence-naturality-epsilon.tikz}}
\end{equation}

We first show the left square commutes.

$\FunG \circ \FunF = \id_{\CatC}$

$\FunG(\FunF(f)) = \FunG(\MorD{f}) = f = \id_{\CatD}(f)$

Note that Proposition <ref> shows that
the composite $\FunG \circ \FunF$ is actually equal to the identity
functor, and thus $\eta_A = \id_A$.

Now we prove the right square commutes.
This proof is somewhat more involved: unlike
<ref>, the composite $\FunF \circ \FunG$ is
merely isomorphic to the identity functor, not equal on the nose.
Thus, we begin with an inductive definition:

We define the natural isomorphism

$\epsilon : \FunF \circ \FunG \to \id_{\CatD}$
for the composite $\FunF \circ \FunG$ inductively:

\begin{equation}
\begin{aligned}
\epsilon_{\unitD}               & \defeq \adapterInv &= \tikzfig{generator-adapterInv-bare} \\
\epsilon_{\ObjD{A}}             & \defeq \id_{\ObjD{A}} &= \tikzfig{id} \\
\epsilon_{\ObjD{A} \TensorD R}  & \defeq \AdapterInv \cp (\id_{\ObjD{A}} \TensorD \epsilon_R) &= \tikzfig{definition-epsilon-recursive}
\end{aligned}
\end{equation}

If $\epsilon$ is natural for $f$ and $g$, then it is natural for $f \cp g$.

Take morphisms $f : X \to Y$ and $g : Y \to Z$.
By assumption, we have:

\[ \FunF(\FunG(f)) = \epsilon_X \cp f \cp \epsilon_Y^{-1} \]

\[ \FunF(\FunG(g)) = \epsilon_Y \cp g \cp \epsilon_Z^{-1} \]

from which we can derive

\begin{equation}
\begin{aligned}
\epsilon_X^{-1} \cp \FunF(\FunG(fg)) \cp \epsilon_Z
&= \epsilon_X^{-1} \cp \FunF(\FunG(f) \cp \FunG(g)) \cp \epsilon_Z \\
&= \epsilon_X^{-1} \cp \FunF(\FunG(f)) \cp \FunF(\FunG(g)) \cp \epsilon_Z \\
&= \epsilon_X^{-1} \cp \epsilon_X \cp f \cp \epsilon_Y^{-1} \cp \epsilon_Y \cp g \cp \epsilon_Z^{-1} \cp \epsilon_Z \\
&= f \cp g \\
\end{aligned}
\end{equation}

as required.

$\FunF \circ \FunG \cong \id_{\CatD}$

With natural isomorphisms $\eta = \id$ and $\epsilon$ as in Definition <ref>.

We proceed by induction, having already proven the inductive step for
composition in Proposition <ref>.
We again use Proposition <ref>–that each
morphism in $\CatD$ can be decomposed into `slices'

\[ t = t_1 \cp \ldots \cp t_n \]

with each $t_i$ of the form $\id_X \TensorD g_i \TensorD \id_Y$, with $g : A \to B$ a generator.
It thus suffices to prove that

\[ \epsilon^{-1}_{X \TensorD A \TensorD Y} \cp \FunF(\FunG(t)) \cp \epsilon_{X \TensorD B \TensorD Y} \]

One can check this by a second induction whose base case and inductive step correspond
to the definition of $\FunG$ (Definition <ref>).
To be precise, one can check this property graphically for each base case
$\FunG(\id_{\ObjD{\unitC}}) \ldots \FunG(\id_{\ObjD{A}})$,
and additionally for the inductive step $\FunG(\id_{\ObjD{A}} \TensorD q \TensorD r)$.

(Mac Lane's Strictness Theorem)

For any monoidal category $\CatC$ there is a monoidally equivalent strict category.

$\FunF$ and $\FunG$ are monoidal functors by Propositions
<ref> and <ref>,
and they form a monoidal equivalence by Propositions
<ref> and
Since $\CatC$ was arbitrary, the proof is complete.

Note that in contrast to Mac Lane's proof of Theorem <ref>,
we make no reference to the coherence theorem.
We can therefore make use of the strictness theorem to prove coherence, which is
the subject Section <ref>.

§ COHERENCE

We can now give an elementary proof of Mac Lane's coherence theorem.

In [13], Mac Lane gives his theorem in two parts:
Theorem 1 <cit.> and its corollary <cit.>.

The `meat' of the proof is in the former part, corresponding to our Section
<ref>, while our Section <ref>
corresponds to Mac Lane's corollary.

Mac Lane begins by defining a certain preorder $\cat{W}$, which he then shows
enjoys the following property:

(Mac Lane's Coherence Theorem, <cit.>)

Let $\cat{M}$ be an arbitrary monoidal category, and let $M$ be an object of $\cat{M}$.
Then there is a unique strict monoidal functor $\CatW \to \cat{M}$ such that
$W \mapsto M$.

In contrast, we will define $\CatW$ so this unique functor is easy to construct,
and then use $\CatSW$ to give a graphical proof that $\CatW$ is a

§.§ The free monoidal category on one generator

We begin by defining $\CatW$. Again, recall that our definition differs from Mac
Lane; we will later show that this definition indeed yields a preorder in order
to guarantee that we indeed prove the same theorem.

We define $\CatW$ as the monoidal category freely generated by a single object
$W$ and no morphisms save for those required by the definition of a monoidal
[Mac Lane denotes the generating object as $(-)$ to suggest an “empty place”.
We follow Peter Hines' convention [9] and use $W$ instead.]

The objects of $\CatW$ are $\unit_{\CatW}$, $W$, and their tensor products.
The arrows are $\id, \rho, \lambda, \alpha$ and their composites and tensor products.

It is now clear that the statement of Mac Lane's Theorem 1 holds for our definition of $\CatW$:

Given an arbitrary monoidal category $\cat{M}$ and object $M \in \cat{M}$,
there is a unique strict monoidal functor $\CatW \to \cat{M}$ with $W \mapsto M$.

Suppose $\FunU : \CatW \to \cat{B}$ is such a (strict) monoidal functor.
Then we must have that:

* $\FunU(W) = B$ (by assumption)

* $\FunU(\unit) = \unit$ (Because $\FunU$ is strict)

* $\FunU(A \otimes B) = \FunU(A) \otimes \FunU(B)$ (because $\FunU$ is strict)

* $\FunU(f) = f$ for $f$ one of $\{\assoc, \unitl, \unitr, \id \}$ (because $\FunU$ is strict)

* $\FunU(f \otimes g) = \FunU(f) \otimes \FunU(g)$ (because $\FunU$ is strict)

But this accounts for all objects and morphisms of $\CatW$, and so $\FunU$ must be unique.

However, to constitute a proof of the strictness theorem we must now prove that
$\CatW$ is a preorder.

Our argument proceeds in three main steps. We will show the following:

* For any monoidal category $\CatC$, If $\CatD$ is a preorder, then so is $\CatC$

* $\CatSW$ is generated solely by adapters $\{ \Adapter, \adapter \}$ and their inverses.

* $\CatSW$ is a preorder (which we prove graphically)

The first two steps are straightforward; we address them now. The third requires
more work, and is contained in Section <ref>.

If is a preorder, then so is $\CatC$.

Let $f, g : \CatC(A, B)$.
Recall that $\FunG \circ \FunF = \id$, and so we can derive

\[ f = \FunG(\FunF(f)) = \FunG(\FunF(g)) = g \]

Where we used that $\FunF(f) = \FunF(g)$ because $\CatD$ is a preorder.

Another lemma shows we can reason about $\CatSW$ by considering only adapters:

$\CatSW$ is generated by $\Adapter, \adapter$ and their inverses.

Arrows of $\CatSW$ are by definition either adapters $\Adapter, \adapter$, their inverses,
or morphisms $\MorD{f}$ for some $f \in \CatW$.
But note that all such $f \in \CatW$ are either $\id, \rho, \lambda, \alpha$ or their composites.
It is clear that each of $\unitl, \unitr, \assoc$ can each be written as
adapters by equations (<ref>), so it remains
to show that composites of such morphisms can also be written this way.

That is, we must show that $\FunF(f \otimes g)$ can be expressed using only
adapters and their composites.
This can be proved inductively: if $\FunF(f), \FunF(g)$ can be expressed using adapters,
then so too can compositions $\FunF(f \cp g) = \FunF(f) \cp \FunF(g)$
and tensors $\FunF(f \otimes g) = \Adapter \cp (\FunF(f) \TensorD \FunF(g)) \cp \AdapterInv$.

Thus every morphism of $\CatSW$ can be expressed in terms of adapters,
and so the category can be said to be generated by (only) adapters.

§.§.§ Graphical proof that $\CatSW$ is a preorder

We can now prove graphically that $\CatSW$ is a preorder using a normal form argument.
Our approach is as follows:

* Define for each object a $\objsize$ in $\Nat$ (Definition <ref>)

* Prove all morphisms in $\CatSW$ go between objects of the same size (Proposition <ref>)

* Define a canonical arrow $\canonical(A, B)$ between any two objects of the same size (Definition <ref>)

* Show that any arrow is equal to the canonical one (Proposition <ref>)

Note that we make heavy use of Proposition
<ref>, which lets us reason about
$\CatSW$ inductively in terms of adapters and their tensors and composites.

We begin–following Mac Lane–by defining the size of an object[
Our $\objsize{}$ is the same notion as Mac Lane's length <cit.>
] as follows:

We define the $\objsize$ of an object as the number of occurrences of $W$, defined inductively:

\begin{align*}
\objsize(\unitSW)             & \defeq 0 \\
\objsize(\ObjD{\unitW})       & \defeq 0 \\
\objsize(\ObjD{W})            & \defeq 1 \\
\objsize(\ObjD{A \TensorC B}) & \defeq \objsize(A) + \objsize(B) \\
\objsize(X \TensorD Y)        & \defeq \objsize(X) + \objsize(Y)
\end{align*}

$\CatSW$ morphisms preserve $\objsize$

If $f : A \to B$ is a morphism in $\CatSW$, then $\objsize(A) = \objsize(B)$.

Induction on morphisms.

We will define the canonical arrow $\canonical(A, B)$ in two halves, $\objpack$ and $\objunpack$.

To do so, we will first need some additional definitions.

We define the `packing' and `unpacking' morphisms $\objpack$ and $\objunpack$ in terms of objects of $\CatSW$.
Let $A \in \CatSW$ be an object.
Then $\objpack(A)$ is the morphism defined inductively as follows:

\begin{align*}
\objpack(\unitSW)              & \quad \defeq \quad \tikzfig{empty} \\
\objpack(\ObjD{\unitW})        & \quad \defeq \quad \tikzfig{pack-adapter} \\
\objpack(\ObjD{W})             & \quad \defeq \quad \tikzfig{pack-id} \\ % TODO: add type
% \Adapter \cp (\objpack(A) \TensorD \objpack(B)) \\ % : \ObjD{\unitW}^{\objsize(A)} % TODO
\objpack(\ObjD{A \TensorC B})  & \quad \defeq \quad \tikzfig{pack-tensorc} \\
% \objpack(X) \TensorD \objpack(Y) % : \ObjD{\unitW}^{\objsize(A)} % TODO
\objpack(X \TensorD Y)         & \quad \defeq \quad \tikzfig{pack-tensord}
\end{align*}

And define $\objunpack(A)$ as $\objpack(A)^{-1}$.

It can be more intuitive to define $\objunpack$ first, thinking of it as the
adapter which removes extraneous $\unitC$ objects and `normalises' the object
into a flat array of $\ObjD{W}$ objects.
In this view, $\objpack$ is the adapter morphism taking a fixed number of
$\ObjD{W}$ objects and assembling them into a certain bracketing, with unit
objects inserted as appropriate.

In Definition <ref> we implicitly used that $\CatSW$ is a
groupoid to define $\objunpack$. This is straightforward to prove:

$\CatSW$ is a groupoid

Generators and identities have inverses by Definition
which allows an inductive definition for tensor and composition, i.e.:

\[ (f \cp g)^{-1} = g^{-1} f^{-1} \]

\[ (f \TensorD g)^{-1} = f^{-1} \TensorD g^{-1} \]

Now, in order to define the canonical arrow as a composition of $\objpack$ and
$\objunpack$, we will need the following lemma which states that for objects
of the same size, we can compose their $\objunpack$ and $\objpack$ morphisms.

$\objpack(A) : \ObjD{W}^{\objsize(A)} \to A$

In other words, for an object $A$ of size $n$, the domain of $\objpack(A)$ is
the $n$-fold $\TensorD$-tensoring of $\ObjD{W}$.

Simple induction on objects (the domain of each $\objpack(A)$ is either $\unitSW$, $\ObjD{W}^k$ or a tensoring of terms)

To each pair of objects $A$, $B$ of the same size, we can define a canonical arrow as follows:

\[ \canonical(A, B) \defeq \objunpack(A) \cp \objpack(B) \]

Note that the composition of Definition <ref> is well-typed because
$\objsize(A) = \objsize(B)$ by Proposition <ref>:

\begin{align*}
\cod(\objunpack(A)) & = \ObjD{W}^{\objsize(A)} \\
& = \ObjD{W}^{\objsize(B)} \\
& = \dom(\objpack(B))
\end{align*}

The canonical arrow between $W \TensorW (\unitW \TensorW W)$ and $(W \TensorW
\unitW) \TensorW W$ is

\[ \tikzfig{example-canonical-associator-with-unit-in-center} \]

Note that this is equal to the associator $\assoc_{W, \unitW, W}$.

We can now show that every morphism $f : A \to B$ in $\CatSW$ is equal to
$\canonical(A, B)$.

For all $f : A \to B$ in $\CatSW$

\[ f = \objunpack(A) \cp \objpack(B) \]

By induction.
On the base case–generators–the proof is straightforward; we give it for
identities and generators g-adapter and g-Adapter,
with the proofs for inverse generators following by a symmetric argument.

\begin{align*}
\canonical(X, X)
& = \objunpack(X) \cp \objpack(X) \\
& = \objpack(X)^{-1} \cp \objpack(X) \\
& = \id_{X} \\
\canonical(\unitSW, \ObjD{\unitW})
& = \objunpack(\unitSW) \cp \objpack(\ObjD{\unitW}) \\
& = \tikzfig{empty} \cp \tikzfig{g-s-adapter} \\
& = \tikzfig{g-s-adapter} \\
\canonical(\ObjD{A} \TensorD \ObjD{B}, \ObjD{A \TensorC B})
& = \objunpack(\ObjD{A} \TensorD \ObjD{B}) \cp \objpack(\ObjD{A \TensorC B}) \\
& = \tikzfig{proof-preorder-base-case-Adapter-1} \\
& = \tikzfig{g-s-Adapter}
\end{align*}

The composition of canonical morphisms is canonical:

\begin{align*}
\canonical(X, Y) & \cp \canonical(Y, Z) \\
& = \objunpack(X) \cp \objpack(Y) \cp \objunpack(Y) \cp \objpack(Z) \\
& = \objunpack(X) \cp \objpack(Y) \cp \objpack(Y)^{-1} \cp \objpack(Z) \\
& = \objunpack(X) \cp \objpack(Z) \\
& = \canonical(X, Z)
\end{align*}

And so is the tensor product:

\begin{align*}
\canonical(X_1, Y_1) & \TensorD \canonical(X_2, Y_2) \\
& = \scalebox{0.8}{\tikzfig{proof-preorder-tensor-1}} \\
& = \scalebox{0.8}{\tikzfig{proof-preorder-tensor-2}} \\
& = \canonical(X_1 \TensorD X_2, Y_1 \TensorD Y_2)
\end{align*}

$\CatSW$ is a preorder

By Proposition <ref> we know that all morphisms
$f : A \to B$ have the property that $\objsize(A) = \objsize(B)$.
We then define for any such objects a canonical morphism $\canonical(A, B)$ in
Definition <ref>.
This canonical isomorphism is unique by Definition <ref>,
and so $\CatSW$ is a preorder.

Since we have now proven that $\CatSW$ is a preorder, it is now straightforward
to prove Theorem <ref>.
Note that this is essentially the opposite of the approach taken by Mac Lane,
who defines a preorder, and then shows the existence of a unique strict
monoidal functor.

(Proof of Theorem <ref>)

By Proposition  there
is a unique, strict monoidal functor from $\CatW$ to an arbitrary monoidal
category $\CatM$ with $W \mapsto A$ for some $A \in \CatM$.
Moreover, $\CatSW$ is a preorder, and so by Proposition
<ref>, so is $\CatW$.

A first consequence of the coherence theorem is that
$\FunG$ is a strict inverse to $\FunF$ for morphisms
$f : \ObjD{A} \to \ObjD{B}$.

If $f : \ObjD{A} \to \ObjD{B}$ then $\FunF(\FunG(f)) = f$

We know that for any $A \in \CatW$ that $\FunG(\ObjD{A}) = A$.
Thus for $f : \ObjD{A} \to \ObjD{B}$ we have $\FunG(f) : A \to B$
and thus $\FunF(\FunG(f)) : \ObjD{A} \to \ObjD{B}$.
But $\CatSW$ is a preorder, so we have
$\FunF(\FunG(f)) = f$.

Proposition <ref> guarantees that any morphism
of this type formed from adapters genuinely represents a specific morphism in
$\CatD$ built from associators and unitors; we will later use this fact to
restate the coherence theorem in terms of adapter morphisms.

§.§ Mac Lane's Corollary

We can now state and prove Mac Lane's corollary <cit.> to the coherence

Note that whereas this proof of the corollary is just a reformulation of Mac
Lane's argument in diagrammatic terms, the previous proof of Theorem
<ref> differs significantly.

Let us begin with an informal statement of the theorem.

Take a commuting diagram of $\CatW$, for instance the triangle axiom below:

\begin{equation}
\label{equation:example-catw-triangle}
\begin{tikzpicture}[node distance=2cm]
\node (A) [					 ] {$W \TensorC (\unitC \TensorC W)$};
\node (B) [right of=A] {};
\node (C) [right of=B] {$(W \TensorC \unitC) \TensorC W$};
\node (D) [below of=B] {$W \TensorC W$};

\draw [->,thick] (A) to [] node[above] {$\assoc_{W,\unitC,W}$} (C);
\draw [->,thick] (A) to [] node[below left ] {$\id_W \TensorC \unitl_W$} (D);
\draw [->,thick] (C) to [] node[below right] {$\unitr_W \TensorC \id_W$} (D);
\end{tikzpicture}
\end{equation}

The coherence theorem allows one to `export' this diagram to an arbitrary
monoidal category $\CatM$ by replacing each $i^{th}$ occurrence of W in a vertex
with some $A_i$ in $\CatM$.
For instance, let $A$ and $B$ be $\CatM$ objects, then we substitute the
first occurrence of $W$ in each vertex for $A$, and the second for $B$, giving
us the following commuting diagram in $\CatM$:

\begin{equation}
\label{equation:example-catm-triangle}
\begin{tikzpicture}[node distance=2cm]
\node (A) [					 ] {$A \TensorC (\unitC \TensorC B)$};
\node (B) [right of=A] {};
\node (C) [right of=B] {$(A \TensorC \unitC) \TensorC B$};
\node (D) [below of=B] {$A \TensorC B$};

\draw [->,thick] (A) to [] node[above] {$\assoc_{A,\unitC,B}$} (C);
\draw [->,thick] (A) to [] node[below left ] {$\id_A \TensorC \unitl_B$} (D);
\draw [->,thick] (C) to [] node[below right] {$\unitr_A \TensorC \id_B$} (D);
\end{tikzpicture}
\end{equation}

The coherence theorem does not say that diagrams in
$\CatM$ whose edges are components of natural transformations all commute;
only those which correspond to diagrams in $\CatW$.  Put another way, if we
have parallel $\CatM$-arrows $f, g : A \to B$ such that $f, g$ are constructed
from associators and unitors, we may not in general conclude that $f = g$.

Now, it is not immediately obvious how even this informal coherence result
follows from the statement of Theorem <ref>.

Although for some fixed object $X \in \CatM$ there is a unique, strict monoidal
functor $\FunU : \CatW \to \CatM$,
this does not let us obtain every diagram we would like.
In particular, using $\FunF$ in this way we cannot obtain diagrams with multiple
variables such as (<ref>)–only those where
every $W$ is replaced by $X$.

To allow for diagrams with multiple variables, Mac Lane constructs the
non-strict monoidal category $\ItM$.

This will allow us to regard objects $A \in \CatW$ of size $n$ as functors
by applying the monoidal functor $\FunU(A) : \CatM^n \to \CatM$ as follows:

\begin{align}
\label{equation:u-catw-to-itm}
\unitM        & \quad \mapsto \quad \tikzfig{generator-functor-adapter} \nonumber \\
W             & \quad \mapsto \quad \tikzfig{generator-functor-id} \\
A \TensorW B  & \quad \mapsto \quad \tikzfig{generator-functor-recursive} \nonumber
\end{align}

In the above, $\tikzfig{g-functor-const}$ denotes the constant functor
$\functor{Const}_{\unit} : \CatT \to \CatM$ mapping the single object of $\CatT$
to the monoidal unit $\unitM$.

Now, $\FunU : \CatW \to \ItM$ preserves diagrams since it is a functor, and so
we may picture the triangle axiom in $\ItM$ graphically as follows:

\[ \scalebox{0.8}{\tikzfig{example-triangle-axiom-graphically}} \]

Where vertices (in blue) depict functors, and edges depict natural
This transformation of $\CatW$-objects to functors formalises the intuition of
`replacing the $i^{th}$ occurrence of $W$ in a diagram'.
That is, for a given diagram in $\CatW$ with vertices $V_i$ of size $n$,
we now simply make a particular choice of $\CatM^n$-object for each vertex
and apply $\FunU(V_i) : \CatM^n \to \CatM$ to obtain a `multivariable' diagram
in $\CatM$.

For completeness, we can now define $\ItM$ and show how it is monoidal.

$\ItM$ (from <cit.>)

Fix an arbitrary monoidal category $(\CatM, \TensorM, \unitM, \assoc, \unitl, \unitr)$.
Then $\ItM$ is the category with:

* Objects: functors $\CatM^n \to \CatM$

* Arrows: natural transformations

With $\CatM^n$ denoting the $n$-fold product $\CatM \times \overset{n}{\ldots} \times \CatM$

The use of our graphical notation above is justified because $\ItM$ forms a
monoidal category in the following way.

$\ItM$ is a (non-strict) monoidal category (from <cit.>)

The monoidal unit is the constant functor $\functor{Const}_{\unit} : \CatT \to \CatM$.
The monoidal product $\TensorItM : \ItM \times \ItM \to \ItM$ is defined on
objects (functors) as:

\[ \Functor{F} \TensorItM \Functor{G} = \tikzfig{itm-tensor-objects} \]

and pointwise on arrows
$\eta : \Functor{F}_1 \to \Functor{G}_1$ and
$\mu : \Functor{F}_2 \to \functor{G}_2$
so that for $\Functor{F}_1, \Functor{G}_1 : \CatM^n \to \CatM$
and $\Functor{F}_2, \Functor{G}_2 : \CatM^m \to \CatM$
the component at $A \times B \in \CatM^n \times \CatM^m$ is

\begin{align*}
(\eta \TensorItM \mu)_{A \times B}
& = \scalebox{0.9}{\tikzfig{itm-tensor-arrows-lhs}} \\
& = \scalebox{0.9}{\tikzfig{itm-tensor-arrows-rhs}}
\end{align*}

Associators and unitors are similarly defined pointwise, i.e.:

\begin{align*}
\unitl_{\Functor{F}_A}
& = \scalebox{0.9}{\tikzfig{itm-unitl-lhs}} \\
& = \scalebox{0.9}{\tikzfig{itm-unitl-rhs}} \\
\unitr_{\Functor{F}_A}
& = \scalebox{0.9}{\tikzfig{itm-unitr-rhs}} \\
\assoc_{{\Functor{F}, \Functor{G}, \Functor{H}}_{A,B,C}}
& = \scalebox{0.9}{\tikzfig{itm-assoc-rhs}} \\
\end{align*}

Associators and unitors are natural since each of their components is natural.
That is, given a natural transformation
$\mu : \Functor{F} \to \Functor{G}$
we know that
$\unitr_\Functor{F} \cp \mu = (\mu \TensorItM \id) \cp \unitr_\Functor{G}$
precisely because components are both sides are always equal, i.e for all $A$ we have
$\unitr_{\Functor{F}_A} \cp \mu_A = (\mu \TensorItM \id)_A \cp \unitr_{\Functor{G}_A}$.
A similar argument applies to $\assoc$ and $\unitl$.
Further, the axioms of monoidal categories are satisfied for the same reason:
each diagram commutes because all its components commute using the
monoidal structure of $\CatM$.

Mac Lane states the coherence result corollary as follows:

(from <cit.>)
Let $\cat{M}$ be a monoidal category. There is a function which assigns to each pair of objects
$A, B \in \CatW$ of $\objsize$ $n$ a (unique) natural isomorphism

\[ \canonical_{\CatM}(A, B) : \FunU(A) \to \FunU(B) \]

called the canonical map from $\FunU(A)$ to $\FunU(B)$,
in such a way that the identity arrow $\unitItM \to \unitItM$ is canonical
(between functors of $0$ variables)
the identity transformation $\id : \id_{\cat{M}} \to \id_{\cat{M}}$ is
$\assoc, \unitl, \unitr$ (and their inverses) are canonical,
and the composite and $\TensorItM$-product of canonical maps is canonical.

(from <cit.>)

Let $\FunU : \CatW \to \ItM$ be the unique strict monoidal functor mapping $W$
to the identity functor $\id : \CatM \to \CatM$ so that $\FunU$ acts on
objects as in (<ref>).
Then $\FunU$ acts on morphisms of $\CatW$ as follows:

\begin{align*}
\id_{\unitW}    & \mapsto \id               \\ % && : \unitItM \to \unitItM \\
\id_{W}         & \mapsto \id               \\ % && : \id_{\CatM} \to \id_{\CatM} \\
\unitl_A        & \mapsto \unitl_{\FunU(A)} \\ % && : \unitItM \TensorItM \FunU(A) \to \FunU(A) \\
\unitr_A        & \mapsto \unitr_{\FunU(A)} \\ % && : \FunU(A) \TensorItM \unitItM \to \FunU(A) \\
\assoc_{A,B,C}  & \mapsto \assoc_{\FunU(A), \FunU(B), \FunU(C)} && \\
f \TensorW g    & \mapsto \FunU(f) \TensorItM \FunU(g) &&
\end{align*}

And so $\canonical_{\CatM}(A, B) = \FunU(f)$ for each unique $f : A \to B$.

Finally, note that the canonical morphism $\canonical_{\CatM}(A, B)$ can be defined as

\[ \canonical_{\CatM}(A, B) = (\FunU \circ \FunG)(\canonical(A, B)) \]

thus we may use the normal form $\canonical(A, B)$ to determine the canonical
natural isomorphism in $\ItM$.

§ CONCLUSIONS

The body of work on string diagrams in general is broad and growing rapidly.
It is therefore slightly surprising that the fundamental issue of non-strict tensorial composition has been neglected for so long.
On the one hand, this is reasonable.
The assumption of strictness does not entail a loss of generality, as indeed we have confirmed via an example in Sec. <ref>.
However, non-strict tupling is a basic feature of programming languages, and even hardware description languages, and modelling it using string diagrams requires the proper mathematical framework.

This framework, the main contribution of the paper, is given in Def. <ref>, which shows a way to strictify a possibly non-strict monoidal category.
The body of the paper proves that the definition has all the desired properties and, int the process, we discuss two new proofs for Mac Lane's strictness and coherence theorems, respectively.
We believe that, as is usually the case, the string-diagrammatic perspective has pedagogical value, lending new concrete intuitions to what otherwise seems like very abstract symbolic exercises.

§.§ Further work

Lack of support for non-strict tensor limits the range of many applications of string diagrams.
The first immediate question to study is whether the strictification recipe we give is compatible with hierarchical string diagrams (`functorial boxes' [14]) which can be used in the representation of monoidal-closed and cartesian-closed categories.
This, in turn, makes them useful for applications to programming languages with higher-order functions, such as high-level circuit synthesis [7] or automatic differentiation [1], which currently do not offer support for product.
Similar considerations motivate the study of strictification of trace monoidal categories, which can be used as models of digital circuits [8].

Further, our construction expands the use of datastructures and algorithms
currently limited only to the strict case (e.g., [17]).
Such datastructures are typically based on graph or hypergraph representations
for performance reasons; applying our construction allows us to leverage those benefits essentially for free.
In cases where such datastructures and algorithms are proven correct, it may be
beneficial to reproduce the proofs in this paper in a formal theorem prover in
order to provide end-to-end verification of applications.

Finally, a formal understanding of non-strict monoidal categories may also open the door of more graphical approaches to theorem proving.
Interactive graphical theorem provers using string diagrams for strict monoidal categories, such as <homotopy.io> represent a refreshingly new approach to the design of proof assistants.
Since models of, for example, intuitionistic logic are non-strict, the novel string diagrams we introduce in this paper could be used perhaps to develop similar graphical proof assistant for more conventional logics.

[1]
Mario Alvarez-Picallo, Dan R. Ghica, David Sprunger, and Fabio Zanasi.
Functorial string diagrams for reverse-mode automatic
CoRR, abs/2107.13433, 2021.

[2]
R.F. Blute, J.R.B. Cockett, R.A.G. Seely, and T.H. Trimble.
Natural deduction and coherence for weakly distributive categories.
Journal of Pure and Applied Algebra, 113(3):229–296, 1996.

[3]
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi.
Full abstraction for signal flow graphs.
In Sriram K. Rajamani and David Walker, editors, Proceedings of
the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 515–526.
ACM, 2015.

[4]
Bob Coecke, Edward Grefenstette, and Mehrnoosh Sadrzadeh.
Lambek vs. lambek: Functorial vector space semantics and string
diagrams for lambek calculus.
Ann. Pure Appl. Log., 164(11):1079–1100, 2013.

[5]
Bob Coecke and Aleks Kissinger.
Picturing quantum processes: A first course in quantum theory
and diagrammatic reasoning.
Cambridge University Press, 2017.

[6]
P. I. Etingof, Shlomo Gelaki, Dmitri Nikshych, and Victor Ostrik, editors.
Tensor categories.
Number volume 205 in Mathematical surveys and monographs. American
Mathematical Society, 2015.

[7]
Dan R. Ghica.
Geometry of synthesis: a structured approach to VLSI design.
In Martin Hofmann and Matthias Felleisen, editors, Proceedings
of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363–375.
ACM, 2007.

[8]
Dan R. Ghica, Achim Jung, and Aliaume Lopez.
Diagrammatic semantics for digital circuits.
In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual
Conference on Computer Science Logic, CSL 2017, August 20-24, 2017,
Stockholm, Sweden, volume 82 of LIPIcs, pages 24:1–24:16. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017.

[9]
Peter Hines.
Coherence and strictification for self-similarity, 2015.

[10]
A. Joyal and R. Street.
Braided tensor categories.
Advances in Mathematics, 102(1):20–78, 1993.

[11]
André Joyal and Ross Street.
The geometry of tensor calculus, i.
Advances in Mathematics, 88(1):55–112, 1991.

[12]
Yves Lafont.
Towards an algebraic theory of Boolean circuits.
Journal of Pure and Applied Algebra, 184(2-3):257–310,
November 2003.

[13]
Saunders Mac Lane.
Categories for the Working Mathematician.
Springer, 1997.

[14]
Paul-André Melliès.
Functorial boxes in string diagrams.
In Zoltán Ésik, editor, Computer Science Logic, 20th
International Workshop, CSL 2006, 15th Annual Conference of the EACSL,
Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 1–30. Springer, 2006.

[15]
Peter Selinger.
A survey of graphical languages for monoidal categories.
In New structures for physics, pages 289–355. Springer, 2010.

[16]
Stuart Sutherland, Simon Davidmann, and Peter Flake.
SystemVerilog for Design Second Edition: A Guide to Using
SystemVerilog for Hardware Design and Modeling.
Springer Science & Business Media, 2006.

[17]
Paul Wilson and Fabio Zanasi.
The cost of compositionality: A high-performance implementation of
string diagram composition, 2021.

§ SEQUENTIAL NORMAL FORM

The following proposition is well-known (see for example
[12]) and straightforward to prove, but we provide a proof
anyway for completeness.

let $\cat{C}$ be a monoidal category presented by generators $\Sigma$ and some equations.
Then any (finite) term $t$ representing a morphism of $\cat{C}$ can be factored into `slices':

\[ (\id \otimes \epsilon_1 \otimes \id) \cp (\id \otimes \epsilon_2 \otimes \id) \cp \ldots \cp (\id \otimes \epsilon_n \otimes \id) \]

This factorization can be diagrammed as follows:

\[ \scalebox{0.9}{\tikzfig{sequential-normal-form}} \]

Note that in general $X_i \neq X_{i+1}$ and so on- i.e., the generators need not be “aligned” in this factorization.
For example, we can have morphisms like the following:

\[ \scalebox{0.9}{\tikzfig{sequential-normal-form-example}} \]

We proceed by induction on terms.
Let $S_0$ denote the set of terms consisting of identities and generators,
Then let

\[ S_n = S_0 \cup \{ t \cp u | t, u \in S_{n-1} \} \cup \{ t \otimes u | t, u \in S_{n-1} \} \]

It is clear that terms in $S_0$ are already in sequential normal form, so it remains to prove the inductive case,
beginning with composition.
Let $v$ be a term in $S_{n+1}$.
Now by inductive hypothesis, any term in $w \in S_n$ has an equivalent term in sequential normal form, which we'll denote
Now there are three cases:

* If $v \in S_n$, then we have $\hat{v}$ by inductive hypothesis.

* If $v = t \cp u$, then $\hat{t}$ and $\hat{u}$ exist by inductive hypothesis, and we can form $\hat{v} = \hat{t} \cp \hat{u}$.

* If $v = t \otimes u$, then $\hat{v} = (\hat{t} \otimes \id) \cp (\id \otimes \hat{u})$

and the proof is complete.

§ $\FUNG$ IS WELL-DEFINED

In this appendix, we check that $\FunG$ is well-defined with respect to the equations
in Definition <ref>.
Specifically, for each of the monoidal, adapter, and associator/unitor equations
$\mathtt{lhs} = \mathtt{rhs}$, we show that $\FunG(\mathtt{lhs}) =
\FunG(\mathtt{rhs})$, and so $\FunG$ is equal under any rewrite involving those

We begin with the functor equations (<ref>)

\begin{align*}
\FunG(\MorD{\id_A}) = \id_A = \FunG(\id_{\ObjD{A}})
\end{align*}

\begin{align*}
\FunG(\MorD{f} \cp \MorD{g}) = \FunG(\MorD{f}) \cp \FunG(\MorD{g}) = f \cp g = \FunG(\MorD{f \cp g})
\end{align*}

Now the adapter equations (<ref>):

\begin{align*}
\FunG(\Adapter \cp (\MorD{f} \TensorD \MorD{g}) \cp \AdapterInv)
& = \FunG(\Adapter) \cp \FunG(\MorD{f} \TensorD \MorD{g}) \cp \FunG(\AdapterInv) \\
& = \FunG(\MorD{f} \TensorD \MorD{g}) \\
& = \FunG(\MorD{f} \TensorD \id) \cp \FunG(\id \TensorD \MorD{g}) \\
& = (f \TensorC \id) \cp (\id \TensorC g) \\
& = f \TensorC g \\
& = \FunG(\MorD{f \TensorC g}) \\
\end{align*}

\begin{align*}
\FunG(\AdapterInv \cp \MorD{f \TensorC g} \cp \AdapterInv)
& = \FunG(\AdapterInv) \cp \FunG(\MorD{f \TensorC g}) \cp \FunG(\Adapter) \\
& = \FunG(\MorD{f \TensorC g}) \\
& = f \TensorC g \\
& = (f \TensorC \id) \cp (\id \TensorC g) \\
& = \FunG(\MorD{f} \TensorD \id) \cp \FunG(\id \TensorD \MorD{g}) \\
& = \FunG((\MorD{f} \TensorD \id) \cp (\id \TensorD \MorD{g})) \\
& = \FunG(\MorD{f} \TensorD \MorD{g}) \\
\end{align*}

\begin{align*}
\FunG(\adapter \cp \adapterInv)
& = \FunG(\adapter) \cp \FunG(\adapterInv) \\
& = \id_{\unitC} \cp \id_{\unitC} \\
& = \id_{\unitC} \\
& = \FunG(\id_{\unitD}) \\
\end{align*}

\begin{align*}
\FunG(\adapterInv \cp \adapter)
& = \FunG(\adapterInv) \cp \FunG(\adapter) \\
& = \id_{\unitC} \cp \id_{\unitC} \\
& = \id_{\unitC} \\
& = \FunG(\MorD{\id_{\unitC}}) \\
& = \FunG(\id_{\ObjD{\unitC}}) \\
\end{align*}

Finally the associator/unitor equations (<ref>):

\begin{align*}
\FunG(\AdapterInv \cp (\id \TensorD \AdapterInv) & \cp (\Adapter \TensorD \id) \cp \Adapter) \\
& = \FunG(\AdapterInv) \cp \FunG(\id \TensorD \AdapterInv) \cp \FunG(\Adapter \TensorD \id) \cp \FunG(\Adapter) \\
& = \id \cp \id \cp \assoc \cp \id \\
& = \assoc \\
& = \FunG(\MorD{\assoc}) \\
\end{align*}

\begin{align*}
\FunG(\AdapterInv \cp (\AdapterInv \TensorD \id) & \cp (\id \TensorD \Adapter) \cp \Adapter) \\
& = \FunG(\AdapterInv) \cp \FunG(\AdapterInv \TensorD \id) \cp \FunG(\id \TensorD \Adapter) \cp \FunG(\Adapter) \\
& = \id \cp \assocInv \cp \id \cp \id \\
& = \assocInv \\
& = \FunG(\MorD{\assocInv}) \\
\end{align*}

\begin{align*}
\FunG(\AdapterInv \cp (\adapterInv \TensorD \id))
& = \FunG(\AdapterInv) \cp \FunG(\adapterInv \TensorD \id) \\
& = \id \cp \unitl \\
& = \unitl \\
& = \FunG(\MorD{\unitl}) \\
\end{align*}

\begin{align*}
\FunG((\adapter \TensorD \id) \cp \Adapter)
& = \FunG(\adapter \TensorD \id) \cp \FunG(\Adapter) \\
& = \unitlInv \cp \id \\
& = \unitlInv \\
& = \FunG(\MorD{\unitlInv}) \\
\end{align*}

\begin{align*}
\FunG(\AdapterInv \cp (\id \TensorD \adapterInv))
& = \FunG(\AdapterInv) \cp \FunG(\id \TensorD \adapterInv) \\
& = \id \cp \unitr \\
& = \unitr \\
& = \FunG(\MorD{\unitr}) \\
\end{align*}

\begin{align*}
\FunG((\id \cp \adapter) \cp \Adapter)
& = \FunG(\id \cp \adapter) \cp \FunG(\Adapter) \\
& = \unitrInv \cp \id \\
& = \unitrInv \\
& = \FunG(\MorD{\unitrInv}) \\
\end{align*}

Thus $\FunG$ is well-defined with respect to the monoidal equations.