Library CT.Instance.Category.Monoidal

A monoidal category is the vertical categorification of the set theory concept of a Monoid (such as that defined in CT.Algebra.Monoid). A monoidal category is a category $C$ together with a functor $C \times C \to C$ which performs the tensor product, an identity element $I$ which lives in $C$, and three natural isomorphisms which serve to force associativity of the tensor operator, and that $I$ acts as a left and right identity. The coherence conditions about the natural isomorphisms give rise to laws known as the triangle identity and the pentagon identity.