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