> 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)\\), which is exactly the logical rule of [hypothetical syllogism](https://en.wikipedia.org/wiki/Hypothetical_syllogism). (Alternatively, it's the same shape as composing two arrows.)

Yup, there's an analogue of the [Curry-Howard-Lambek correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Curry%E2%80%93Howard%E2%80%93Lambek_correspondence) for linear logic and symmetric closed monoidal categories.

John Baez and Mike Stay go into this in [*Physics, topology, logic and computation: a Rosetta Stone (2011)*](http://arxiv.org/abs/0903.0340). Another nice discussion is in Abramsky and Tzevelekos' [*Introduction to Categories and Categorical Logic* (2011)](https://arxiv.org/pdf/1102.1313.pdf).

Yup, there's an analogue of the [Curry-Howard-Lambek correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Curry%E2%80%93Howard%E2%80%93Lambek_correspondence) for linear logic and symmetric closed monoidal categories.

John Baez and Mike Stay go into this in [*Physics, topology, logic and computation: a Rosetta Stone (2011)*](http://arxiv.org/abs/0903.0340). Another nice discussion is in Abramsky and Tzevelekos' [*Introduction to Categories and Categorical Logic* (2011)](https://arxiv.org/pdf/1102.1313.pdf).