
Monoidal
Categories
Title: 
Monoidal Categories 
Author:

Eugene W. Stark (stark /at/ cs /dot/ stonybrook /dot/ edu)

Submission date: 
20170504 
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. 
Change history: 
[20170518]:
Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter.
(revision 015543cdd069)
[20180529]:
Modifications required due to 'Category3' changes. Introduced notation for "in hom".
(revision 8318366d4575)

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

License: 
BSD License 
Depends on: 
Category3 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

