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 \\)

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 \\)