Note: This page is about an alternative presentation of monads. There is a different notion of “extension system” that is to a bicategory what a closed category is to a monoidal category; for this, see closed category.
An extension system is a way of presenting a monad that doesn’t involve iteration of the underlying endofunctor. This is simpler for certain purposes, and the operations involved are more basic to some applications such as monads in computer science.
From (Marmolejo-Wood 10):
there is an important overarching reason to consider monads in this way. Extension systems allow us to completely dispense with the iterates $[$…$]$ of the underlying arrow. No iteration is necessary. A moment’s reflection on the various terms of terms and terms of terms of terms that occur in practical applications suggest that this alone justies the alternate approach. $[$…$]$ we note that extension systems in higher dimensional category theory provide an even more important simplication of monads. For even in dimension 2, some of the tamest examples are built on pseudofunctors that are difficult to iterate.
An extension system (Marmolejo-Wood 10) on a category $C$ consists of
For every object $A\in C$, an object $T A\in C$ and a morphism $\eta_A \colon A\to T A$, and
For every morphism $f\colon B\to T A$ in $C$, a morphism $f^T \colon T B \to T A$, satisfying the following axioms:
For every $A$ we have $(\eta_A)^T = 1_{T A}$,
For every $f \colon B\to T A$, we have $f^T \circ \eta_B = f$, and
For every $f \colon B\to T A$ and $g:C \to T B$, we have $f^T \circ g^T = (f^T \circ g)^T$.
Given these data, we make $T$ a functor by $T f = (\eta_A \circ f)^T$, we define multiplication maps $\mu_A:T T A \to T A$ as $(1_{T A})^T$, and we verify that the result is a monad. Conversely, given a monad $(T,\eta,\mu)$, we define $f^T = \mu_A \circ T f$ and check the above axioms. Thus, extension systems are equivalent to monads.
This presentation of a monad is especially convenient for defining the Kleisli category $C_T$: its objects are those of $C$, its morphisms $B\to A$ are the morphisms $B\to T A$ in $C$, and the composite of $f:B\to T A$ with $g:C \to T B$ is $f^T \circ g$.
It is also possible to define algebras over a monad using this presentation. A $T$-algebra consists of
An object $B$, and
For every morphism $h:X\to B$, a morphism $h^B : T X \to B$, such that
For every $h:X\to B$ we have $h^B \circ \eta_X = h$, and
For every $h:X\to B$ and $y:Y\to T X$ we have $h^B \circ y^T = (h^B \circ y)^B$.
When $C$ is a cartesian closed category, to make $T$ a strong monad we simply have to enhance the extension operation $(-)^T$ to an internal morphism $(T A)^B \to (T A)^{T B}$, or equivalently $T B \times (T A)^B \to T A$. This morphism is known as “bind” in use of monads in computer science.
The above definitions are from
but the definition of monad as extension system appeared in
and this definition and also the definition of algebras by an extension operation appeared in
See also
F. Marmolejo and R. J. Wood, Kan extensions and lax idempotent pseudomonads, TAC 2012
F. Marmolejo and R. J. Wood, No-iteration pseudomonads, TAC 2013
The definition of monad as an extension system was used by Eugenio Moggi (and referred to as a “Kleisli triple”) in his original paper introducing the application of monads in computer science for modeling different notions of computation:
This way of presenting a monad is also closely related to continuation-passing style, as described in
Last revised on May 28, 2018 at 04:11:35. See the history of this page for a list of all contributions to it.