By the way, we're starting to use a fact we may not have proved. Let's prove it! It's not hard, but it's good to be fill in all the details.

First, suppose \\(\mathcal{V}\\) is a monoidal preorder. It's easy to show there is a monotone function

\[ a \otimes - : \mathcal{V} \to \mathcal{V} \]

that sends any \\(x \in \mathcal{V} \\) to \\(a \otimes x \in \mathcal{V}\\). To see that it's monotone we just need to show

\[ x \le y \text{ implies } a \otimes x \le a \otimes y .\]

But this follows from the definition of monoidal poset: the tensor product is monotone in each argument!


**Theorem.** Suppose \\(\mathcal{V}\\) is a monoidal poset. Show that \\(\mathcal{V}\\) is closed iff for every element \\(x \in \mathcal{V}\\) the monotone function \\(x \otimes -: \mathcal{V} \to \mathcal{V}\\) has a right adjoint.

**Puzzle.** Prove this theorem!

You get to use this definition:

**Definition.** A monoidal poset is **closed** if for all elements \\(x,y \in \mathcal{V}\\) there is an element \\(x \multimap y \in \mathcal{V}\\) such that

\[ x \otimes a \le y \text{ if and only if } a \le x \multimap y \]

for all \\(a \in \mathcal{V}\\).

The theorem is _almost_ obvious, but there's one thing to check that you may not have checked. Also:

**Puzzle.** In a closed monoidal poset, is the element \\(x \multimap y\\) unique? Can you guess why I'm using posets instead of preorders here?