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_.

> > 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_.