> Interesting, in a class on sub-structural they used / and \ for ordered implication/closure.

A closed monoidal poset that happens to be lattice is called [*residuated lattice*](https://en.wikipedia.org/wiki/Residuated_lattice#Definition).

Some textbooks (and Wikipedia) denote \$$x \multimap z\$$ with \$$x / z\$$ and call it the *right residual of \$$z\$$ by \$$x\$$*. Dually they denote \$$z ⟜ y\$$ as the *left residual of \$$z\$$ by \$$y\$$* and it is denoted with \$$z \backslash y\$$.

The "lollipop" \$$\multimap\$$ was, AFAIK, introduced by Jean-Yves Girard in [*Linear Logic* (1987)](https://www.sciencedirect.com/science/article/pii/0304397587900454). Just as fragments of intuitionistic logic can be given semantics in *Cartesian Closed Categories* (CCC)s, the \$$\otimes,\multimap\$$-fragement of linear logic can be given semantics in *Symmetric Monoidal Closed Categories* (SMCCs). There is a nice discussion of this in [*Introduction to Categories and Categorical Logic (2011)*](https://arxiv.org/pdf/1102.1313.pdf) by Abramsky and Tzevelekos.