Email Gateway (Aug 22 2022 at 15:26): Email Gateway (Aug 22 2022 at 15:26):From: Tobias Nipkow <nipkow@in.tum.de>
Monoidal Categories
Eugene W. Stark
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.
https://www.isa-afp.org/entries/MonoidalCategory.shtml
Enjoy!
smime.p7s
Last updated: Oct 31 2025 at 08:28 UTC