Closed monoidal category
In mathematics, especially in category theory, a closed monoidal category (or a "monoidal closed category") is a category that is both a monoidal category and a closed category in such a way that the structures are compatible. A classic example is the category of sets, Set, where the monoidal product of sets formula_1 and formula_2 is the usual cartesian product formula_3, and the internal Hom formula_4 is the set of functions from formula_1 to formula_2. A non-cartesian example is the category of vector spaces, "K"-Vect, over a field formula_7. Here the monoidal product is the usual  tensor product of vector spaces, and the internal Hom is the vector space of linear maps from one vector space to another. The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system. Many examples of closed monoidal categories are symmetric. However, this need not always be the case, as non-symmetric monoidal categories can be encountered in category-theoretic formulations of linguistics; roughly speaking, this is because word-order in natural language matters. Definition. A closed monoidal category is a monoidal category formula_8 such that for every object formula_2 the  functor given by right tensoring with formula_2 has a right adjoint, written This means that there exists a bijection, called 'currying', between the Hom-sets that is natural in both "A" and "C". In a different, but common notation, one would say that the functor has a right adjoint Equivalently, a closed monoidal category formula_8 is a category equipped, for every two objects "A" and "B", with satisfying the following universal property: for every morphism there exists a unique morphism such that It can be shown that this construction defines a functor formula_22. This functor is called the internal Hom  functor, and the object formula_23 is called the internal Hom of formula_1 and formula_2. Many other notations are in common use for the internal Hom. When the tensor product on formula_8 is the cartesian product, the usual notation is formula_4 and this object is called the exponential object. Biclosed and symmetric categories. Strictly speaking, we have defined a right closed monoidal category, since we required that "right" tensoring with any object formula_1 has a right adjoint. In a left closed monoidal category, we instead demand that the functor of left tensoring with any object formula_1 have a right adjoint A  biclosed monoidal category is a monoidal category that is both left and right closed. A symmetric monoidal category is left closed if and only if it is right closed. Thus we may safely speak of a 'symmetric monoidal closed category' without specifying whether it is left or right closed. In fact, the same is true more generally for braided monoidal categories: since the braiding makes formula_32 naturally isomorphic to formula_33, the distinction between tensoring on the left and tensoring on the right becomes immaterial, so every right closed braided monoidal category becomes left closed in a canonical way, and vice  versa. We have described closed monoidal categories as monoidal categories with an extra property. One can equivalently define a closed monoidal category to be a closed category with an extra property. Namely, we can demand the existence of a tensor product that is left adjoint to the internal Hom functor. In this approach, closed monoidal categories are also called monoidal closed categories.