Hey Chris,

Looks like you've got some formatting problems.

I think I can show your conjecture in certain cases.

For a *closed* monoidal preorder \$$\mathcal{V}\$$ as defined in [Lecture 60](https://forum.azimuthproject.org/discussion/2287/lecture-60-chapter-4-closed-monoidal-posets) we can turn \$$\mathcal{V}\$$ into a \$$\mathcal{V}\$$-enriched category by defining \$$\mathcal{V}(x,y) = x \multimap y \$$. This does the trick...

**Lemma**. Let \$$\mathcal{V}\$$ be a closed monoidal preorder. Then

$\mathcal{X}(x,x') \otimes \mathcal{Y}(y,y') \otimes \mathcal{X}(x',x'') \otimes \mathcal{Y}(y',y'') \le \mathcal{X}(x,x'') \otimes \mathcal{Y}(y,y'') \tag{★}$

for all \$$\mathcal{V}\$$-categories \$$\mathcal{X}\$$ \$$\mathcal{Y}\$$ and objects \$$x,x',x'',y,y'\$$ and \$$y''\$$ if and only if \$$\mathcal{V}\$$ is commutative.

**Proof.**

\$$(\Longleftarrow)\$$ This direction follows from applying condition (b) of the definition of \$$\mathcal{V}\$$-category in [Lecture 29](https://forum.azimuthproject.org/discussion/2121/lecture-29-chapter-2-enriched-categories), and the fact that \$$- \otimes X\$$ is a monotone function for all \$$X\$$.

\$$(\Longrightarrow)\$$ Given (★) and \$$\mathcal{V}\$$ is closed, we need to show \$$\mathcal{V}\$$ is commutative.

To this end, let \$$\mathcal{X}(a,b) = \mathcal{Y}(a,b) = a \multimap b \$$. Furthermore let \$$x = x' = y = I\$$ and \$$y' = y''\$$. Plugging all of this into (★) gives:

$(I \multimap I) \otimes (I \multimap y'') \otimes (I \multimap x'') \otimes (y'' \multimap y'') \le (I \multimap x'') \otimes \mathcal{Y}(1,y'') \tag{★★}$

Since \$$\mathcal{V}\$$ is closed, we know \$$(z \otimes -) \dashv (z \multimap -) \$$. We can use this adjunction to prove a couple of identities:

$\begin{eqnarray} & z \multimap z = I \\\\ & I \multimap z = z \end{eqnarray}$

(I won't prove these here, but I'll show them if anyone is curious.)

Using these two rules and \$$I \otimes z = z \otimes I = z\$$, then (★★) simplifies to:

$y'' \otimes x'' \le x'' \otimes y''$

It follows immediately that \$$y'' \otimes x'' = x'' \otimes y''\$$, so we know that \$$\mathcal{V}\$$ is commutative.\$$\qquad \blacksquare \$$