Monoidal Categories

 

Title: Monoidal Categories
Author: Eugene W. Stark (stark /at/ cs /dot/ stonybrook /dot/ edu)
Submission date: 2017-05-04
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.
BibTeX:
@article{MonoidalCategory-AFP,
  author  = {Eugene W. Stark},
  title   = {Monoidal Categories},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2017,
  note    = {\url{http://isa-afp.org/entries/MonoidalCategory.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Category3