Showing changes from revision #2 to #3:
Added | Removed | Changed
An imploid is a preordered set equipped with an “implication” operation and unit, satisfying certain axioms of “composition”, “identity”, and “unit”. One motivation for studying imploids is that they arise naturally from directed monoids (or “dmonoids”), where the associativity and unit axioms are postulated in only one direction. Another motivation is that imploids provide an appropriate notion of typing for linear lambda calculus?. Finally, in a certain sense imploids can be seen as a natural generalization of groups.
Imploids can also be called “skew-closed preorders”, being the preorder case of the concept of a skew-closed category in the sense of Street (2013). (Similarly, dmonoids can be called “skew-monoidal preorders”, being the preorder case of the concept of a skew-monoidal category (Szlachanyi 2012).)
An imploid is a preordered set equipped with:
and which satisfies the composition law:
for all ; and
for all .
An imploid is said to be undirected if the underlying preorder is symmetric, so that (2)-(4) also hold in the converse direction. On the other hand, the imploid is said to be commutative if it additionally satisfies an exchange law:
for all . Finally, in any imploid we have that implies ; we say that the imploid is normalized if the converse is also true.
Any group can be seen as an undirected (normalized) imploid, by taking the preorder to be the equality relation and defining . In this case, the composition law (2) holds because
while the identity and unit laws (3) and (4) likewise follow immediately from the group axioms.
(See article dmonoid for the definition.)
It is well-known that if has the structure of a monoidal category and for every object , the tensor functor has a right adjoint , then can also be given the structure of a closed category. But what about the converse? In other words, if is a closed category and every functor has a left adjoint, is also a monoidal category? It turns out that the answer is no, because in general the associator maps
are not necessarily invertible, i.e., they only establish associativity up to natural transformation, and not up to natural isomorphism.
(cf. Street 2013): If is a dmonoid for which each operation () has a right adjoint operation , then is also an imploid. Conversely, if is an imploid for which each operation has a left adjoint operation , then is also a dmonoid.
Any dmonoid induces an imploid whose elements are the downsets of ordered by inclusion, and where the implication and unit are defined by:
Any imploid induces a dmonoid whose elements are the upsets of ordered by reverse inclusion, and where the multiplication and unit are defined by:
nlab: closed category
B. J. Day and M. L. Laplaza, On Embedding Closed Categories, Bull. Austral. Math. Soc. 18 (1978), 357-371.
Ross Street. Skew-closed categories. Journal of Pure and Applied Algebra 217(6) (June 2013), arXiv:1205.6522
Kornel Szlachanyi. Skew-monoidal categories and bialgebroids. arXiv:1201.4981