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 .
