Abstract: 
Building on the formalization of basic category theory set out in the
author's previous AFP article, 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 et al, 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.

BibTeX: 
@article{MonoidalCategoryAFP,
author = {Eugene W. Stark},
title = {Monoidal Categories},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{https://isaafp.org/entries/MonoidalCategory.html},
Formal proof development},
ISSN = {2150914x},
}
