### 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.

### License

BSD License

### History

July 10, 2020
  Added new material on cartesian monoidal categories. (revision 06640f317a79)
February 15, 2020
  Cosmetic improvements. (revision a51840d36867)
May 29, 2018
  Modifications required due to 'Category3' changes. Introduced notation for "in hom". (revision 8318366d4575)
May 18, 2017
  Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter. (revision 015543cdd069)

### Topics

- Mathematics/Category theory

### Session MonoidalCategory

- MonoidalCategory
- MonoidalFunctor
- FreeMonoidalCategory
- CartesianMonoidalCategory

### Depends on

- Category Theory with Adjunctions and Limits

### Used by

- Bicategories

## Cite

×

MonoidalCategory-AFP

    @article{MonoidalCategory-AFP,
      author  = {Eugene W. Stark},
      title   = {Monoidal Categories},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/MonoidalCategory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- May 5, 2017 : Isabelle2016-1