imploid in Noam Zeilberger

#Contents#
* table of contents
{:toc}

## Idea

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)](#Street2013). (Similarly, dmonoids can be called "skew-monoidal preorders", being the preorder case of the concept of a _skew-monoidal category_ [(Szlachanyi 2012)](#Szlachanyi2012).)

## Definition

An **imploid** is a preordered set $(X,\le)$ equipped with:

1. a binary operation $\multimap$ (called _implication_) which is _contravariant_ in its first argument and _covariant_ in its second argument:
\[
  \label{clopsetbifunctor}
  \array{
  \arrayopts{\rowlines{solid}}
  a_2 \le a_1 \quad b_1 \le b_2 \\
  a_1\multimap b_1 \le a_2\multimap b_2
  }
\]
and which satisfies the **composition law**:
\[
  \label{clopsetcomposition}
  b \multimap c \le (a \multimap b) \multimap (a \imp c)
\]
for all $a,b,c \in X$; and
2. an element $I \in X$ (called _unit_) satisfying *identity* and *unit laws*:
\[
  \label{clopsetidentity}
  I \le a \multimap a
\]
\[
  \label{clopsetunit}
  I \multimap a \le a
\]
for all $a \in X$.

An imploid is said to be **undirected** if the underlying preorder is symmetric, so that (eq:clopsetcomposition)-(eq:clopsetunit) also hold in the converse direction.
On the other hand, the imploid is said to be **commutative** if it additionally satisfies an **exchange law**:
\[
  \label{clopsetexchange}
  a \multimap (b \multimap c) \le b \multimap (a \multimap c)
\]
for all $a,b,c \in X$.
Finally, in any imploid we have that $a \le b$ implies $I \le a \multimap b$; we say that the imploid is **normalized** if the converse is also true.

## Examples

### From a group

Any group $G = (G,\cdot,I,(-)^{-1})$ can be seen as an undirected (normalized) imploid, by taking the preorder to be the equality relation and defining $a \multimap b \mathbin{:=} b\cdot a^{-1}$. In this case, the composition law (eq:clopsetcomposition) holds because
$$
b \multimap c =
c b^{-1} = 
c a^{-1} a b^{-1} = 
(a \multimap b) \multimap (a \multimap c)
$$
while the identity and unit laws (eq:clopsetidentity) and (eq:clopsetunit) likewise follow immediately from the group axioms.

## Relating imploids and dmonoids

(See article [[dmonoid]] for the definition.)

### dmonoidal imploid = imploidal dmonoid

It is well-known that if $C$ has the structure of a [[nlab:monoidal category]] and for every object $a \in C$, the tensor functor $-\otimes a : C \to C$ has a right adjoint $-\otimes a\dashv [a,-]$, then $C$ can also be given the structure of a [[nlab:closed category]]. But what about the converse? In other words, if $C$ is a closed category and every functor $[a,-]$ has a left adjoint, is $C$ also a monoidal category? It turns out that the answer is **no**, because in general the [[nlab:associator]] maps

$$\alpha_{a,b,c} : (a \otimes b)\otimes c \to a \otimes (b\otimes c)$$

are not necessarily invertible, i.e., they only establish associativity up to natural _transformation_, and not up to natural isomorphism.

+-- {: .num_prop }
###### Proposition

(cf. Street 2013): 
If $M = (M,\le,\cdot,I)$ is a dmonoid for which each operation $-\cdot a : M \to M$ ($a \in M$) has a right adjoint operation $a \multimap - : M \to M$, then $M$ is also an imploid.
Conversely, if $P = (P,\le,\multimap,I)$ is an imploid for which each operation $a \multimap - : P \to P$ has a left adjoint operation $-\cdot a : P \to P$, then $P$ is also a dmonoid.

=--

## Related concepts

* [[dmonoid]]

## References

* {#DayLaPlaza78} B. J. Day and M. L. Laplaza, On Embedding Closed Categories, _Bull. Austral. Math. Soc._ 18 (1978), 357-371.

* {#Street2013} Ross Street. Skew-closed categories. _Journal of Pure and Applied Algebra_ 217(6) (June 2013), [arXiv:1205.6522](https://arxiv.org/abs/1205.6522)

* {#Szlachanyi2012} Kornel Szlachanyi. Skew-monoidal categories and bialgebroids. [arXiv:1201.4981](https://arxiv.org/abs/1201.4981)