Jonathan wrote:

> > but by the definition of closed this is true if and only if

> > $x \otimes (x \multimap y) \otimes (y \multimap z) \le z.$

> It's interesting to note that by the definition of being closed, this is the same as \$$(x \multimap y) \otimes (y \multimap z) \le (x \multimap z)\$$....

That's not so surprising, since that's what I was in the midst of proving. I was trying to prove

$(x \multimap y) \otimes (y \multimap z) \le (x \multimap z)$

and the only way to make progress was to note that this is equivalent to

$x \otimes (x \multimap y) \otimes (y \multimap z) \le z.$

> ... which is exactly the logical rule of hypothetical syllogism. (Alternatively, it's the same shape as composing two arrows.)

Yes, that's more interesting!

$(x \multimap y) \otimes (y \multimap z) \le (x \multimap z)$

says that we can compose morphisms in a closed monoidal category viewed as enriched over itself... and it's also a rule of logic: "if x implies y and y implies z then x implies z". That's because most systems of logic _are_ closed monoidal categories!

Category theory unifies everything! I hadn't known this rule was called [hypothetical syllogism](https://en.wikipedia.org/wiki/Hypothetical_syllogism).

The Lemma in this lecture is a version of _modus ponens_.