Closed monoidal category

A non-cartesian example is the category of vector spaces, K-Vect, over a field

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.

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

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[citation needed] that this construction defines a functor

Many other notations are in common use for the internal Hom.

is the cartesian product, the usual notation is

Strictly speaking, we have defined a right closed monoidal category, since we required that right tensoring with any object

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

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.