nLab relevant monad

Idea

A relevant monad is a special kind of monad which is related to relevance logic.

Definition

Let $\mathcal{C}$ be a category with Cartesian products. Let $(T, \mu,\eta)$ be a monad on $\mathcal{C}$.

Recall that $T$ is said to be right-strong with respect to the Cartesian product (see strong monad) if it is equipped with a natural transformation $\alpha_{X,Y} : T(X)\times Y\to T(X\times Y)$ satisfying some coherence conditions which can be found on the linked page.

In what follows, fix a monad $(T, \mu,\eta)$ together with a choice of right strength $\alpha$ for the Cartesian product.

Using the symmetry isomorphism of the Cartesian product it is possible to give a left strength $\alpha'_{A,B} : A\times T(B)\to T(A\times B)$ by

$$A\times T(B) \cong T(B)\times A \xrightarrow{\alpha_{B,A}}T(B\times A)\cong T(A\times B)$$

Definition

Let $T$ be a strong monad. The right double-strength on $T$ is the natural transformation

$$dst_{X,Y} : T(X)\times T(Y)\xrightarrow{\alpha_{X,T(Y)}}T(X\times T(Y))\xrightarrow{T(\alpha^{'}_{X,Y})}T^2(X\times Y)\xrightarrow{\mu}T(X\times Y)$$

Definition

If $(T,\mu,\eta)$ is a right-strong monad with respect to the Cartesian product, then $T$ is said to be relevant if the following diagrammatic law holds:

References

Concept was first introduced here, see Prop 2.2:

• Anders Kock, Bilinearity and Cartesian-Closed Monads In: Mathematica Scandinavica 29.2 (1971), pp. 161–74. JSTOR: 24491025, pdf

Jacobs is probably the first one to introduce the name ‘relevant monad’:

• Bart Jacobs, Semantics of Weakening and Contraction In: Annals of

  Pure and Applied Logic 69.1 (Sept. 1994), pp. 73–106. issn: 01680072. doi: 10.1016/0168-0072(94)90020-5

See also:

• Louis Parlant et al., Preservation of Equations by Monoidal Monads, July 7, 2020, arXiv: 2001.06348 [cs, math]