Closed monoidal category

A (right) closed monoidal category is a category which is both monoidal and closed in a compatible way. The compatibility condition is given by currying, which is to say we have an adjunction

for every object , inducing a bijection

natural in all objects . It turns out that whenever the tensor product of a monoidal category possesses such a right adjoint, we automatically get all the structure of a closed category, hence we may characterize a monoidal closed category as a monoidal category whose product has a right adjoint.

Evaluation and coëvaluation

The coünit of adjunction is called evaluation and has components

whereas the unit is called coëvaluation and has components

question

I suspect both of these can be shown to be extranatural in .

#state/develop | #lang/en | #SemBr