Ordered logic

Ordered logic is the internal language of non-symmetric monoidal categories. As with linear and nonlinear logic, if the ordered logic contains function-types then they correspond to internal-homs making the monoidal category closed, although one has to be a bit careful since in the non-symmetric case there are two inequivalent notions of internal-hom; sometimes one speaks of "left closed" and "right closed" to distinguish, with either "closed" or "biclosed" when both are present.