\documentclass[11pt,notitlepage,a4paper]{report}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym,eufrak}
\usepackage[english]{babel}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% XYPic package, for drawing commutative diagrams.
\input{xy}
\xyoption{curve}
\xyoption{arrow}
\xyoption{matrix}
%\xyoption{2cell}
%\UseAllTwocells

% Even though I stayed within the default boundary in the JEdit buffer,
% some proof lines wrap around in the PDF document.  To minimize this,
% increase the text width a bit from the default.
\addtolength\textwidth{60pt}
\addtolength\oddsidemargin{-30pt}
\addtolength\evensidemargin{-30pt}

\begin{document}

\title{Monoidal Categories}
\author{Eugene W. Stark\\[\medskipamount]
        Department of Computer Science\\
        Stony Brook University\\
        Stony Brook, New York 11794 USA}
\maketitle

\begin{abstract}
Building on the formalization of basic category theory set out in the author's
previous AFP article \cite{Category3-AFP}, the present article formalizes
some basic aspects of the theory of monoidal categories.
Among the notions defined here are monoidal category, monoidal functor,
and equivalence of monoidal categories.
The main theorems formalized are MacLane's coherence theorem and the
constructions of the free monoidal category and free strict monoidal category
generated by a given category.
The coherence theorem is proved syntactically, using a structurally recursive
approach to reduction of terms that might have some novel aspects.
We also give proofs of some results given by Etingof {\em et al}
\cite{Etingof15}, which may prove useful in a formal setting.
In particular, we show that the left and right unitors need not be taken as
given data in the definition of monoidal category, nor does the definition of
monoidal functor need to take as given a specific isomorphism expressing the
preservation of the unit object.
Our definitions of monoidal category and monoidal functor are stated so as
to take advantage of the economy afforded by these facts.

Revisions made subsequent to the first version of this article added material on
cartesian monoidal categories; showing that the underlying category of a cartesian
monoidal category is a cartesian category, and that every cartesian category
extends to a cartesian monoidal category.
\end{abstract}

\tableofcontents

\chapter{Introduction}

A {\em monoidal category} is a category $C$ equipped with a
binary ``tensor product'' functor $\otimes: C \times C \rightarrow C$,
which is associative up to a given natural isomorphism,
and an object ${\cal I}$ that behaves up to isomorphism like
a unit for $\otimes$.  The associativity and unit isomorphisms are
assumed to satisfy certain axioms known as {\em coherence conditions}.
Monoidal categories were introduced by B\'{e}nabou \cite{Benabou63} and
MacLane \cite{MacLane63}.  MacLane showed that the axioms for a monoidal
category imply that all diagrams in a large class are commutative.
This result, known as MacLane's Coherence Theorem, is the first important
result in the theory of monoidal categories.

Monoidal categories are important partly because of their ubiquity.
The category of sets and functions is monoidal; more generally any category
with binary products and a terminal object becomes a monoidal category if we
take the categorical product as $\otimes$ and the terminal object as ${\cal I}$.
The category of vector spaces over a field, with linear maps as morphisms,
not only admits monoidal structure with respect to the categorical product,
but also with respect to the usual tensor product of vector spaces.
Monoidal categories serve as the starting point for enriched category theory
in that they provide a setting in which ordinary categories,
having ``homs in the category of sets,'' can be generalized to
``categories having homs in a monoidal category ${\cal V}$''.
In addition, the theory of monoidal categories can be regarded as a
stepping stone to the theory of bicategories, as monoidal categories are
the same thing as one-object bicategories.

Building on the formalization of basic category theory set out in the author's
previous AFP article \cite{Category3-AFP}, the present article formalizes
some basic aspects of the theory of monoidal categories.
In Chapter \ref{monoidal-category-chap}, we give a definition of the
notion of monoidal category and develop consequences of the axioms.
We then give a proof of MacLane's coherence theorem.  The proof is syntactic:
we define a language of terms built from arrows of a given category $C$
using constructors that correspond to formal composition and tensor product
as well as to the associativity and unit isomorphisms and their formal inverses,
we then define a mapping that interprets terms of the language in an arbitrary
monoidal category $D$ via a valuation functor $V: C \rightarrow D$,
and finally we syntactically characterize a class of equations between terms
that hold in any such interpretation.  Among these equations are all those that
relate formally parallel ``canonical'' terms, where a term is canonical if
the only arrows of $C$ that are used in its construction are identities.
Thus, all formally parallel canonical terms have identical interpretations
in any monoidal category, which is the content of MacLane's coherence theorem.

In Chapter \ref{monoidal-functor-chap}, we define the notion of a
{\em monoidal functor} between monoidal categories.
A monoidal functor from a monoidal category $C$ to a monoidal category $D$
is a functor $F: C \rightarrow D$, equipped with additional data that
express that the monoidal structure is preserved by $F$ up to natural isomorphism.
A monoidal functor is {\em strict} if it preserves the monoidal structure
``on the nose'' ({\em i.e.}~the natural isomorphism is an identity).
We also define the notion of an {\em equivalence of monoidal categories},
which is a monoidal functor $F: C \rightarrow D$ that is part of an ordinary
equivalence of categories between $C$ and $D$.

In Chapter \ref{fmc-chap}, we use the language of terms defined in
Chapter \ref{monoidal-category-chap} to give a syntactic construction
of the free monoidal category ${\cal F}C$ generated by a category $C$.
The arrows ${\cal F}C$ are defined to be certain equivalence classes of terms,
where composition and tensor product, as well as the associativity and
unit isomorphisms, are determined by the syntactic operations.
After proving that the construction does in fact yield a monoidal category,
we establish its freeness: every functor from $C$ to a monoidal category $D$
extends uniquely to a strict monoidal functor from ${\cal F}C$ to $D$.
We then consider the subcategory ${\cal F}_S C$ of ${\cal F}C$ whose arrows
are equivalence classes of terms that we call ``diagonal.''
Diagonal terms amount to lists of arrows of $C$, composition in ${\cal F}_S C$
is given by elementwise composition of compatible lists of arrows,
and tensor product in ${\cal F}_S C$ is given by concatenation of lists.
We show that the subcategory ${\cal F}_S C$ is monoidally equivalent to
the category ${\cal F} C$ and in addition that ${\cal F}_S C$ is the free
strict monoidal category generated by ${\cal C}$.

The formalizations of the notions of monoidal category and monoidal functor
that we give here are not quite the traditional ones.  The traditional
definition of monoidal category assumes as given not only an ``associator''
natural isomorphism, which expresses the associativity of the tensor product,
but also left and right ``unitor'' isomorphisms, which correspond to unit laws.
However, as pointed out in \cite{Etingof15}, it is not necessary to take the
unitors as given, because they are uniquely determined by the other structure
and the condition that left and right tensoring with the unit object are
endo-equivalences.  This leads to a definition of monoidal category that
requires fewer data to be given and fewer conditions to be verified in
applications.  As this is likely to be especially important in a formal setting,
we adopt this more economical definition and go to the trouble to obtain
the unitors as defined notions.  A similar situation occurs with the
definition of monoidal functor.  The traditional definition requires two
natural isomorphisms to be given: one that expresses the preservation of 
tensor product and another that expresses the preservation of the unit object.
Once again, as indicated in \cite{Etingof15}, it is logically unnecessary
to take the latter isomorphism as given, since there is a canonical definition
of it in terms of the other structure.  We adopt the more economical
definition of monoidal functor and prove that the traditionally assumed
structure can be derived from it.

Finally, the proof of the coherence theorem given here potentially has some
novel aspects.  A typical syntactic proof of this theorem, such as that described
in \cite{MacLane71}, involves the identification, for each term constructed
as a formal tensor product of the unit object ${\cal I}$ and ``primitive objects''
({\em i.e.}~the elements of a given set of generators), of a ``reduction''
isomorphism obtained by composing ``basic reductions'' in which occurrences
of ${\cal I}$ are eliminated using components of the left and right unitors and
``parentheses are moved to one end'' using components of the associator.
The construction of these reductions is performed, as in \cite{MacLane71},
using an approach that can be thought of as the application of an iterative
strategy for normalizing a term.
My thoughts were initially along these lines, and I did succeed in producing
a formal proof of the coherence theorem in this way.  However, proving the
termination of the reduction strategy was complicated by the necessity of using
of a ``rank function'' on terms, and the lemmas required for the remainder of the
proof had to be proved by induction on rank, which was messy.
At some point, I realized that it ought to be possible to define reductions
in a structurally recursive way, which would permit the lemmas in the rest of
the proof to be proved by structural induction, rather than induction on rank.
It took some time to find the right definitions, but in the end this
approach worked out more simply, and is what is presented here.

\medskip\par\noindent
{\bf Revision Notes}

The original version of this document dates from May, 2017.
The current version of this document incorporates revisions made in mid-2020
after the release of Isabelle2020.  Aside from various minor improvements,
the main change was the addition of a new theory, concerning cartesian monoidal categories,
which coordinates with material on cartesian categories that was simultaneously
added to \cite{Category3-AFP}.  The new theory defines ``cartesian monoidal category''
as an extension of ``monoidal category'' obtained by adding additional functors,
natural transformations, and coherence conditions.  The main results proved are that
the underlying category of a cartesian monoidal category is a cartesian category,
and that every cartesian category extends to a cartesian monoidal category.

% include generated text of all theories
\input{session}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
