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 $𝐵 \in 𝖢$ , inducing a bijection

𝖢 (𝐴 \otimes 𝐵, 𝐶) ≅ 𝖢 (𝐴, [𝐵, 𝐶])

natural in all objects $𝐴, 𝐶 \in 𝖢$ . 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

𝜖 𝐵 𝐶 : [𝐵, 𝐶] \otimes 𝐵 \to 𝐶

whereas the unit is called coëvaluation and has components

𝜂 𝐵 𝐶 : 𝐶 \to [𝐵, 𝐶 \otimes 𝐵] .

question

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

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