\section{Introduction}\label{IntroSec}

The concept of basis in mathematics is best known for a vector space.
It involves a way of writing an arbitrary vector $v$ as finite linear
combination $v = \sum_{i} v_{i}e_{i}$, using special base vectors
$e_i$, which are mutually independent. In the current paper this
phenomenon will be studied at a more general level, using algebras and
coalgebras.  A vector space is an algebra --- to be precise, an
Eilenberg-Moore algebra of a particular monad --- and the
decompositions can be described as a coalgebra $v \mapsto \sum_{i}
v_{i}e_{i}$. The fact that bases are coalgebras is the main, novel
observation. It applies to other structures than vector spaces, like
directed complete partial orders and convex sets.

In general, algebras are used for composition and coalgebras for
decomposition.  An algebra $a\colon T(X)\rightarrow X$, for a functor
or a monad $T$, can be used to produce elements in $X$ from
ingredients structured by $T$. Conversely, a coalgebra $c\colon
X\rightarrow T(X)$ allows one to decompose an element in $X$ into its
ingredients with structure according to $T$. This is the fundamental
difference between algebraic and coalgebraic data structures.

Assume an arbitrary category $\cat{A}$, carrying a monad $T$, as
in the lower left corner of the next diagram.
\begin{equation}
\label{MonadIterDiag}
\vcenter{\xymatrix@C-1pc{
& \textsl{Alg}\xspace(T)
   \ar@(ul,ur)^-{\mbox{comonad }\overline{T}}
   \ar[dl]_{\dashv}\ar@/^3.5ex/[dr]
& &
\textsl{Alg}\xspace(-)\ar@{--}[dl]\ar@(ul,ur)^-{\mbox{comonad}}
& & \cdots \\
\quad\cat{A}\quad\ar@(dr,dl)[]^-{\mbox{monad }T}\ar@/^3.5ex/[ur]
& &
\textsl{CoAlg}\xspace(\overline{T})\ar[ul]_{\dashv}
   \ar@(dr,dl)[]^-{\mbox{monad }\overline{\overline{T}}}
& &
\textsl{CoAlg}\xspace(-)\ar[ul]\ar@(dr,dl)[]^-{\mbox{monad}}\ar@{--}[ur] &
}}
\end{equation}

\noindent The category $\textsl{Alg}\xspace(T)$ of algebras of the monad $T$ comes
with a standard adjunction $\textsl{Alg}\xspace(T) \rightleftarrows \cat{A}$. This
adjunction induces a comonad $\overline{T}$ on $\textsl{Alg}\xspace(T)$, see
Section~\ref{ComonadSec} for details. Then we can form the category
$\textsl{CoAlg}\xspace(\overline{T})$ of coalgebras of the comonad $\overline{T}$,
with standard adjunction $\textsl{CoAlg}\xspace(\overline{T}) \leftrightarrows
\textsl{Alg}\xspace(T)$, inducing a monad $\smash{\overline{\overline{T}}}$ on
$\textsl{CoAlg}\xspace(\overline{T})$. This process can be continued, and gives rise
to an alternating sequence of monads and comonads.

This situation~\eqref{MonadIterDiag} has been studied by various
authors, see
\textit{e.g.}~\cite{Barr69,RoseburghW91,Jacobs94b,Kock95}. One obvious
question is: does the sequence~\eqref{MonadIterDiag} stabilise?
Stabilisation after 2 steps is proven in~\cite{Barr69} for monads on
$\Cat{Sets}\xspace$. Here we prove stabilisation in 3 steps for special monads (of
so-called Kock-Z{\"o}berlein type) on $\Cat{PoSets}\xspace$, see below.

But more importantly, here it is proposed that a
$\overline{T}$-coalgebra on a $T$-algebra can be seen as a
\emph{basis} for this algebra, see Section~\ref{ComonadSec}. In
particular, in Section~\ref{SetSec} it will be shown that the concept
of basis in linear algebra gives rise to such a coalgebra
$X\rightarrow\overline{\ensuremath{\mathcal{M}}}(X)$ for the multiset monad $\ensuremath{\mathcal{M}}$; this
coalgebra decomposes an element $x$ of a vector space $X$ into a
formal sum $\sum_{i}x_{i}e_{i}\in\ensuremath{\mathcal{M}}(X)$ given by its coefficients
$x_i$ for a Hamel basis $(e_{i})$, see Theorem~\ref{OperatorCoalgThm}
for more details. In the same vein, the operation that sends an
element of a convex set to a formal convex sum of extreme elements is
an instance of such a coalgebra.

Other examples arise in an order-theoretic setting, see
Section~\ref{OrderSec}.  Here one uses the notion of monad of
Kock-Z{\"o}berlein type --- where $T(\eta_{X}) \leq \eta_{TX}$,
see~\cite{Kock95,Escardo98}. We describe how such monads fit in the
present setting (with continuous dcpos as coalgebras), and add a new
result (Theorem~\ref{KZCoAlgBasisThm}) about
algebras-on-coalgebras-on-algebras, see Section~\ref{OrderSec}.  This
builds on rather old (little noticed) work of the
author~\cite{Jacobs94b}.

The first two steps of the sequence~\eqref{MonadIterDiag} are also
relevant in the semantics of effectful programming based on monads.
In~\cite{Levy06} it is shown that the exception monad transformer is a
monad itself---so it can play the role of $T$
in~(\ref{MonadIterDiag})---and that its algebras provide a syntax for
raising exceptions, whereas the associated coalgebra/basis takes care
of exception handling. These results are intriguing and need to be
tested and investigated further, but that is beyond the scope of this
paper.  We mention them only briefly in Section~\ref{ExceptionSec}.

In recent work~\cite{CoeckePV12} in the categorical foundations of
quantum mechanics it is shown that orthonormal bases in
finite-dimensional Hilbert spaces are equivalent to comonoids
structures (in fact, Frobenius algebras). These como\-noids are used
for copying and deleting elements. In Section~\ref{ComonoidSec} it is
shown how bases as coalgebras (capturing bases-as-decomposition) also
give rise to such comonoids (capturing
bases-as-copier-and-deleter). These comonoids can be used to formulate
in general terms what it means for an endomap to be diagonalised. This
is illustrated for a.o.\ the Pauli functions.

\section{Comonads on categories of algebras}\label{ComonadSec}

In this preliminary section we investigate the situation of a monad
and the induced comonad on its category of algebras. We shall see that
coalgebras of this comonad capture the notion of basis, in a very
general sense. This will be illustrated later in several situations
see in particular Subsection~\ref{VectorSpaceSubsec}.

For an arbitrary monad $T\colon \cat{A} \rightarrow \cat{A}$, with
unit $\eta\colon \idmap \Rightarrow T$ and multiplication $\mu\colon
T^{2} \Rightarrow T$, there is a category $\textsl{Alg}\xspace(T)$ of
(Eilenberg-Moore) algebras, together with a left adjoint $F$ (for free
algebra functor) to the forgetful functor $U\colon
\textsl{Alg}\xspace(T)\rightarrow\cat{A}$. This adjunction $\textsl{Alg}\xspace(T) \leftrightarrows
\cat{A}$ induces a comonad on the category $\textsl{Alg}\xspace(T)$, which we shall
write as $\overline{T} = FU$ in:
\vspace*{-1em}
\begin{equation}
\label{ComonadFromMonadDiag}
\vcenter{\xymatrix@R-.5pc@C-1pc{
& & \\
\textsl{Alg}\xspace(T)\ar[d]_{\dashv}^{U}
   \ar `u[r] `[rd] `[u]^{\overline{T}=FU\;\mbox{\small comonad}} [] & \\
\cat{A}\ar@/^3ex/[u]^{F}\ar `r[rd] `[r]^{T=UF\;\mbox{\small monad}} `[lr] []
   & \\
& &
}}
\end{equation}

\noindent For an algebra $\smash{(TX\stackrel{a}{\rightarrow} X)} \in
\textsl{Alg}\xspace(T)$ there are counit $\varepsilon\colon \overline{T} \Rightarrow
\idmap$ and comultiplication $\delta\colon \overline{T} \Rightarrow
\overline{\overline{T}}$ maps in $\textsl{Alg}\xspace(T)$ given by:
\begin{equation}
\label{ComonadFromMonadStructEqn}
\vcenter{\xymatrix{
\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
& &
\ensuremath{\left(\xy
(0,4)*{T^{2}X};
(0,-4)*{TX};
{\ar^{\mu\rlap{$\scriptscriptstyle{_X}$}} (0,2); (0,-2)};
\endxy\right)}\ar[ll]_-{\varepsilon = a}\ar[rr]^-{\delta = T(\eta_{X})}
& &
\ensuremath{\left(\xy
(0,4)*{T^{3}X};
(0,-4)*{T^{2}X};
{\ar^{\mu_{T\!\rlap{$\scriptscriptstyle X$}}} (0,2); (0,-2)};
\endxy\right)}
}}
\end{equation}

\auxproof{
In general, for an adjunction $F\dashv G$ the induced comonad $FG$
comes with counit $\varepsilon \colon FG \rightarrow \idmap$
inherited from the adjunction and comultiplication $\delta \colon
FG \rightarrow FGFG$ given by $\delta = F\eta G$.

In this case, starting from the free algebra adjunction $F\dashv U$
the unit is the unit of the monad, and the counit $FU \rightarrow
\idmap$, at an algebra, is this algebra itself, as a map of algebras:
$$\xymatrix{
FU\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
= \ensuremath{\left(\xy
(0,4)*{T^{2}X};
(0,-4)*{TX};
{\ar^{\mu_X} (0,2); (0,-2)};
\endxy\right)}\ar[rr]^-{a}
& &
\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
}$$
}

\begin{defi}
\label{BasisDef}
Consider a monad $T \colon \cat{A} \rightarrow \cat{A}$ together with
the comonad $\overline{T} \colon \textsl{Alg}\xspace(T) \rightarrow \textsl{Alg}\xspace(T)$ induced by $T$,
as in~(\ref{ComonadFromMonadDiag}). A \emph{basis} for a $T$-algebra
$\smash{(TX\stackrel{a}{\rightarrow} X) \in \textsl{Alg}\xspace(T)}$ is a
$\smash{\overline{T}}$-coalgebra on this algebra, given by a map of
algebras $b$ of the form:
$$\xymatrix@C-.5pc{
\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}\ar[rr]^-{b}
& &
\overline{T}\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
=
FU\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
=
\ensuremath{\left(\xy
(0,4)*{T^{2}X};
(0,-4)*{TX};
{\ar^{\mu\rlap{$\scriptscriptstyle{_X}$}} (0,2); (0,-2)};
\endxy\right)}
}$$

\noindent Thus, a basis $b$ is a map $\smash{X\xrightarrow{b} TX}$ in
$\cat{A}$ satisfying $b \mathrel{\circ} a = \mu_{X} \mathrel{\circ} T(b)$ and $a \mathrel{\circ}
b = \idmap$ and $T(\eta_{X}) \mathrel{\circ} b = T(b) \mathrel{\circ} b$ in:
$$\xymatrix@R-.5pc{
T(X)\ar[d]_{a}\ar[r]^-{T(b)} & T^{2}(X)\ar[d]^{\mu_X}
& &
X\ar@{=}[dr]\ar[r]^-{b} & T(X)\ar[d]^{\varepsilon = a}
& &
T(X)\ar[r]^-{T(b)} & T^{2}(X) \\
X\ar[r]_-{b} & T(X)
& &
& X
& &
X\ar[u]^-{b}\ar[r]_{b} & T(X)\ar[u]_{\delta=T(\eta_{X})}
}$$
\end{defi}

\noindent As we shall see a basis as described above may be understood as
providing a decomposition of each element $x$ of an algebra into a
collection $b(x)$ of basic elements that together form $x$.  The
actual basic elements $X_{b} \rightarrowtail X$ involved can be
obtained as the indecomposable ones, via the following equaliser in
the underlying category.
\begin{equation}
\label{BasisEqualiserDiag}
\vcenter{\xymatrix@C+1pc{
X_{b}\ar@{ >->}[r]^-{e} & X \ar@<+.5ex>@/^1ex/[r]^-{b}
   \ar@<-.5ex>@/_1ex/[r]_-{\eta} & T\rlap{$(X)$}
}}
\end{equation}

\noindent One can then ask in which cases the map of algebras
$T(X_{b}) \rightarrow X$, induced by the equaliser $e\colon X_{b}
\rightarrow U(TX\rightarrow X)$, is an isomorphism. This is (almost
always) the case for monads on \Cat{Sets}\xspace, see
Proposition~\ref{SetsBasisProp} below. But first we observe that free
algebras always carry a basis.

\begin{lem}
\label{FreeAlgCoalgLem}
Free algebras have a canonical basis: each $\smash{FX =
  \big(T^{2}X \stackrel{\mu}{\rightarrow} TX\big)} \in \textsl{Alg}\xspace(T)$
carries a $\overline{T}$-coalgebra, namely given by $T(\eta_{X})$. This
gives a situation:
$$\xymatrix@C-1pc{
& \textsl{Alg}\xspace(T)
   \ar@(ul,ur)^-{\overline{T}=FU}
   \ar[dl]_{\dashv}
& \\
\cat{A}\ar@(d,l)[]^-{T}\ar@/^3.5ex/[ur]^{F}\ar[rr]_-{F}
   & & \textsl{CoAlg}\xspace\rlap{$(\overline{T})$}\ar[ul]
}$$
\end{lem}

\begin{myproof}
It is easy to check that $T(\eta_{X})$ is a morphism in $\textsl{Alg}\xspace(T)$ and
a $\overline{T}$-coalgebra:
$$\vcenter{\xymatrix{
F(X) = \ensuremath{\left(\xy
(0,4)*{T^{2}X};
(0,-4)*{TX};
{\ar^{\mu\rlap{$\scriptscriptstyle{_X}$}} (0,2); (0,-2)};
\endxy\right)}\ar[rr]^-{T(\eta_{X})}
& &
\ensuremath{\left(\xy
(0,4)*{T^{3}X};
(0,-4)*{T^{2}X};
{\ar^{\mu_{T\!\rlap{$\scriptscriptstyle X$}}} (0,2); (0,-2)};
\endxy\right)} = \overline{T}(FX).
}}\eqno{\qEd}$$

\auxproof{
$$\begin{array}{rcl}
\varepsilon \mathrel{\circ} T(\eta_{X})
& = &
\mu_{X} \mathrel{\circ} T(\eta_{X}) \\
& = &
\idmap \\
\delta \mathrel{\circ} T(\eta_{X})
& = &
T(\eta_{TX}) \mathrel{\circ} T(\eta_{X}) \\
& = &
T(\eta_{TX} \mathrel{\circ} \eta_{X}) \\
& = &
T(T(\eta_{X}) \mathrel{\circ} \eta_{X}) \\
& = &
T^{2}(\eta_{X}) \mathrel{\circ} T(\eta_{X}) \\
& = &
\overline{T}(T(\eta_{X})) \mathrel{\circ} T(\eta_{X}).
\end{array}$$
}
\end{myproof}

\noindent The object $X_b$ of basic elements, as
in~(\ref{BasisEqualiserDiag}), in the situation of this lemma is the
original set $X$ in case the monad $T$ satisfies the so-called
\emph{equaliser requirement}~\cite{Moggi88}, which says precisely that
$\eta_{X} \colon X \rightarrow TX$ is the equaliser of $T(\eta_{X}),
\eta_{TX} \colon TX \rightrightarrows T^{2}X$. This requirement does
\emph{not} hold, for instance, for the powerset monad.

There is some redundancy in the data described in
Definition~\ref{BasisDef}. This is implicitly used in the description
of syntax for exception in~\cite{SchroderM04} (with only `handle' as
coalgebra and no `raise' algebra, see also~\cite{Levy06} and
Section~\ref{ExceptionSec}).

\begin{lem}
Assume a monad $T\colon\cat{A} \rightarrow \cat{A}$, with induced
comonad $\smash{\overline{T}} \colon \textsl{Alg}\xspace(T) \rightarrow \textsl{Alg}\xspace(T)$.
Having:
\begin{iteMize}{$\bullet$}
\item a $T$-algebra $a\colon T(X) \rightarrow X$ together with a
  $\smash{\overline{T}}$-coalgebra $b\colon a \rightarrow
  \overline{T}(a)$
\end{iteMize}

\noindent is the same as having:
\begin{iteMize}{$\bullet$}
\item a map $c\colon X \rightarrow T(X)$ in $\cat{A}$ which forms an
  equaliser diagram in $\cat{A}$:
$$\xymatrix@C+.5pc{
X\ar@{ >->}[r]^-{c} & T(X) \ar@<+.5ex>@/^1ex/[r]^-{T(c)}
   \ar@<-.5ex>@/_1ex/[r]_-{T(\eta)}
    & T(X)
}$$
\end{iteMize}
\end{lem}

\begin{myproof}
Assuming an algebra and coalgebra $(a,b)$ as above, it is easy to check
that $b\colon X\rightarrow T(X)$ is the equaliser of $T(b)$ and
$T(\eta)$.

\auxproof{
Recall that $\delta = T(\eta)$, so $T(\eta) \mathrel{\circ} b = \delta \mathrel{\circ} b
= T(b) \mathrel{\circ} b$. If also $f\colon Y\rightarrow T(X)$ satisfies
$T(b) \mathrel{\circ} f = T(\eta) \mathrel{\circ} f$, then $a \mathrel{\circ} f\colon Y \rightarrow
X$ satisfies:
$$\begin{array}{rcccccl}
b \mathrel{\circ} a \mathrel{\circ} f
& = &
\mu \mathrel{\circ} T(b) \mathrel{\circ} f
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} f
& = &
f.
\end{array}$$

\noindent Moreover, $a \mathrel{\circ} f$ is the only such map: if $g\colon Y
\rightarrow X$ also satisfies $b \mathrel{\circ} g = f$, then $g = a \mathrel{\circ} b
\mathrel{\circ} g = a \mathrel{\circ} f$.
}

The other direction is a bit more work: assume we have $c\colon X
\rightarrow T(X)$ forming an equaliser of $T(c)$ and $T(\eta)$.
Consider the map $a$ defined in the diagram:
$$\xymatrix@C+.5pc@R-.5pc{
X\ar@{ >->}[r]^-{c} & T(X) \ar@<+.5ex>[r]^-{T(c)}\ar@<-.5ex>[r]_-{T(\eta)}
    & T(X) \\
T(X)\ar@{..>}[u]^{a}\ar[r]_-{T(c)} & T^{2}(X)\ar[u]_{\mu}
}$$

\noindent Using the equaliser property one checks that $a$ is a
$T$-algebra, and that $c\colon X\rightarrow T(X)$ satisfies the
$\overline{T}$-coalgebra requirements from
Definition~\ref{BasisDef}. \qed

\auxproof{
First we need to check that the map $\mu \mathrel{\circ} T(c)$ actually
equalises:
$$\begin{array}{rcl}
T(c) \mathrel{\circ} \mu \mathrel{\circ} T(c)
& = &
\mu \mathrel{\circ} T^{2}(c) \mathrel{\circ} T(c) \\
& = &
\mu \mathrel{\circ} T^{2}(\eta) \mathrel{\circ} T(c) \\
& = &
T(\eta) \mathrel{\circ} \mu \mathrel{\circ} T(c).
\end{array}$$

\noindent Further, $a\colon T(X) \rightarrow X$ is an algebra:
$$\begin{array}{rcl}
c \mathrel{\circ} a \mathrel{\circ} \eta
& = &
\mu \mathrel{\circ} T(c) \mathrel{\circ} \eta \\
& = &
\mu \mathrel{\circ} \eta \mathrel{\circ} c \\
& = &
c \\
& = &
c \mathrel{\circ} \idmap \\
c \mathrel{\circ} a \mathrel{\circ} T(a)
& = &
\mu \mathrel{\circ} T(c) \mathrel{\circ} T(a) \\
& = &
\mu \mathrel{\circ} T(\mu \mathrel{\circ} T(c)) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}(c) \\
& = &
\mu \mathrel{\circ} T(c) \mathrel{\circ} \mu \\
& = &
c \mathrel{\circ} a \mathrel{\circ} \mu.
\end{array}$$

\noindent Obviously, $\delta \mathrel{\circ} c = T(c) \mathrel{\circ} c$, since $\delta
= T(\eta)$. By construction of $a$, $c$ is a map of algebras $a
\rightarrow \mu$. Hence we only need to verify:
$$\begin{array}{rcl}
c \mathrel{\circ} a \mathrel{\circ} c
& = &
\mu \mathrel{\circ} T(c) \mathrel{\circ} c \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} c \\
& = &
c \\
& = &
c \mathrel{\circ} \idmap.
\end{array}$$
}
\end{myproof}

The comonad $\overline{T}\colon\textsl{Alg}\xspace(T)\rightarrow\textsl{Alg}\xspace(T)$
from~(\ref{ComonadFromMonadDiag}) gives rise to a category of
coalgebras $\textsl{CoAlg}\xspace(\overline{T})\rightarrow\textsl{Alg}\xspace(T)$, where this
forgetful functor has a right adjoint, which maps an algebra
$TY\rightarrow Y$ to the diagonal coalgebra $\delta\colon\mu_{Y}
\rightarrow\mu_{TY}$ as in~(\ref{ComonadFromMonadStructEqn}).  Thus we
obtain a monad on the category $\textsl{CoAlg}\xspace(\overline{T})$, written as
$\overline{\overline{T}}$, like in the
sequence~\eqref{MonadIterDiag}. On a basis $c\colon a\rightarrow
\overline{T}(a)$, for an algebra $a\colon TX\rightarrow X$, there is a
unit $\eta_{c} = c\colon c\rightarrow\delta$ and multiplication
$\mu_{c} = T(c)\colon \delta\rightarrow\delta$ in
$\textsl{CoAlg}\xspace(\overline{T})$.

\auxproof{
Explicitly, for algebras $a\colon TX\rightarrow X$ and $b\colon
TY\rightarrow Y$ and a basis $c\colon a\rightarrow \overline{T}$
there is a bijective correspondence:
$$\begin{prooftree}
{\xymatrix{
\Big(a\stackrel{c}{\rightarrow}\overline{T}(a)\Big)\ar[r]^-{f} &
   \Big(\mu_{Y}\stackrel{\delta}{\rightarrow}\overline{T}(\mu_{Y})\Big)}}
\Justifies
{\xymatrix{
\Big(TX\stackrel{a}{\rightarrow}X\Big)\ar[r]_-{g} &
   \Big(TY\stackrel{b}{\rightarrow}Y\Big)}}
\end{prooftree}$$

\noindent It is given by:
\begin{iteMize}{$\bullet$}
\item for $f\colon X\rightarrow TY$ take $\overline{f} = b \mathrel{\circ} f$.
It is a map of algebras $a\rightarrow b$ since:
$$\begin{array}{rcll}
b \mathrel{\circ} T(\overline{f})
& = &
b \mathrel{\circ} T(b) \mathrel{\circ} T(f) \\
& = &
b \mathrel{\circ} \mu \mathrel{\circ} T(f) \\
& = &
b \mathrel{\circ} f \mathrel{\circ} a
  & \mbox{since $f$ is a map of algebras $a\rightarrow\mu_Y$} \\
& = &
\overline{f} \mathrel{\circ} a.
\end{array}$$

\item for $g\colon X\rightarrow Y$ take $\overline{g} = T(g) \mathrel{\circ} c$.
This is both a map of algebras $a\rightarrow\mu_{Y}$ and of coalgebras
$c\rightarrow\delta$:
$$\begin{array}{rcll}
\mu \mathrel{\circ} T(\overline{g})
& = &
\mu \mathrel{\circ} T^{2}(g) \mathrel{\circ} T(c) \\
& = &
T(g) \mathrel{\circ} \mu \mathrel{\circ} T(c) \\
& = &
T(g) \mathrel{\circ} c \mathrel{\circ} a
  & \mbox{since $c$ is a map of algebra $a\rightarrow\mu_{Y}$} \\
& = &
\overline{g} \mathrel{\circ} a \\
\delta \mathrel{\circ} \overline{g}
& = &
T(\eta) \mathrel{\circ} T(g) \mathrel{\circ} c \\
& = &
T^{2}(g) \mathrel{\circ} T(\eta) \mathrel{\circ} c \\
& = &
T^{2}(g) \mathrel{\circ} T(c) \mathrel{\circ} c
   & \mbox{since $\delta \mathrel{\circ} c = T(c) \mathrel{\circ} c$} \\
& = &
T(\overline{g}) \mathrel{\circ} c
\end{array}$$
\end{iteMize}

\noindent Finally,
$$\begin{array}{rcl}
\overline{\overline{f}}
& = &
T(\overline{f}) \mathrel{\circ} c \\
& = &
T(b \mathrel{\circ} f) \mathrel{\circ} c \\
& = &
T(b) \mathrel{\circ} \delta \mathrel{\circ} f \\
& = &
T(b \mathrel{\circ} \eta) \mathrel{\circ} f \\
& = &
f \\
\overline{\overline{g}}
& = &
b \mathrel{\circ} \overline{g} \\
& = &
b \mathrel{\circ} T(g) \mathrel{\circ} c \\
& = &
g \mathrel{\circ} a \mathrel{\circ} c \\
& = &
g.
\end{array}$$

In particular, for a $\overline{T}$-coalgebra $c\colon X\rightarrow
T(X)$ on an algebra $a\colon T(X)\rightarrow X$ we have unit $\eta_{c} =
c\colon c\rightarrow\delta$ in $\textsl{CoAlg}\xspace(\overline{T})$ and counit
$\varepsilon_{b} = b\colon \mu\rightarrow b$ in $\textsl{Alg}\xspace(T)$ of this
adjunction $\textsl{CoAlg}\xspace(\overline{T}) \rightleftarrows \textsl{Alg}\xspace(T)$. The induced
monad $\overline{\overline{T}} \colon \textsl{CoAlg}\xspace(\overline{T}) \rightarrow
\textsl{CoAlg}\xspace(\overline{T})$ thus has multiplication $\mu_{c} = T(c)\colon
\delta\rightarrow\delta$ in a situation:
$$\xymatrix{
\Big(\mu_{TX}\stackrel{\delta}{\longrightarrow}\mu_{T^{2}X}\Big)
   \ar[rr]^-{\mu = T(a)} & &
\Big(\mu_{X}\stackrel{\delta}{\longrightarrow}\mu_{TX}\Big)
}$$

\noindent using that $T(a) \mathrel{\circ} \mu_{X} = \mu_{TX} \mathrel{\circ} T^{2}(a)$
and $\delta \mathrel{\circ} T(a) = T(\eta \mathrel{\circ} a) = T(T(a) \mathrel{\circ} \eta) =
T^{2}(a) \mathrel{\circ} \delta$.
}

By iterating this construction as in~\eqref{MonadIterDiag} one obtains
alternating monads and comonads. Such iterations are studied for
instance in~\cite{Barr69,RoseburghW91,Jacobs94b,Kock95}. In special
cases it is known that the iterations stop after a number of
cycles. This happens after 2 iterations for monads on sets, as we
shall see next, and after 3 iterations for Kock-Z{\"o}berlein monads
in Section~\ref{OrderSec}. This stabilisation means that in presence
of sufficiently many iterated (co)algebraic operations, the algebraic
structure that we start from becomes free --- typically on some atoms
or basic elements.

\section{Set-theoretic examples}\label{SetSec}

It turns out that for monads on the category \Cat{Sets}\xspace only free algebras
have bases. This result goes back to~\cite{Barr69}. We repeat it in
the present context, with a sketch of proof.  Subsequently we describe
the situation for the powerset monad (from~\cite{Jacobs94b}), the
free vector space monad, and the distribution monad.

\begin{prop}
\label{SetsBasisProp}
For a monad $T$ on \Cat{Sets}\xspace, if an algebra
$\smash{TX\stackrel{a}{\rightarrow} X}$ has a basis
$\smash{X\stackrel{b}{\rightarrow} \overline{T}X}$ with non-empty
equaliser $X_{b} \rightarrowtail X \rightrightarrows TX$ as
in~(\ref{BasisEqualiserDiag}), then the induced map $T(X_{b})
\rightarrow X$ is an isomorphism of algebras and coalgebras. In
particular, in the set-theoretic case any algebra with a non-empty
basis is free.
\end{prop}

\begin{myproof}
Let's consider the equaliser $X_{b} \rightarrowtail X$ of
$b,\eta\colon X\rightrightarrows T(X)$ from~(\ref{BasisEqualiserDiag}) in
\Cat{Sets}\xspace. It is a so-called coreflexive equaliser, because there is a map
$TX\rightarrow X$, namely the algebra $a$, satisfying $a \mathrel{\circ} b =
\idmap = a \mathrel{\circ} \eta$. It is well-known---see
\textit{e.g.}~\cite[Lemma~6.5]{Mesablishvili06} or the dual result
in~\cite[Volume~I, Example~2.10.3.a]{Borceux94}---that if
$X_{b}\neq\emptyset$ such coreflexive equalisers in \Cat{Sets}\xspace are split,
and thus absolute. The latter means that they are preserved under any
functor application. In particular, by applying $T$ we obtain a new
equaliser in \Cat{Sets}\xspace, of the form:
\begin{equation}
\label{RestrictedBaseDiag}
\vcenter{\xymatrix@R-1pc@C+0.5pc{
T(X_{b})\ar@{ >->}[r]^-{T(e)} & T(X)
   \ar@<+.5ex>[r]^-{T(b)}\ar@<-.5ex>[r]_-{T(\eta) = \delta} & T^{2}(X) \\
X\ar[ur]_{b}\ar@{-->}[u]^{b'}
}}
\end{equation}

\noindent The resulting map $b'$ is the inverse to the adjoint transpose
$a \mathrel{\circ} T(e) \colon T(X_{b}) \rightarrow X$, since:
\begin{iteMize}{$\bullet$}
\item $a \mathrel{\circ} T(e) \mathrel{\circ} b' = a \mathrel{\circ} b = \idmap$;

\item the other equation follows because $T(e)$ is equaliser, and thus
  mono:
$$\begin{array}{rcll}
T(e) \mathrel{\circ} b' \mathrel{\circ} a \mathrel{\circ} T(e)
& = &
b \mathrel{\circ} a \mathrel{\circ} T(e) \\
& = &
\mu \mathrel{\circ} T(b) \mathrel{\circ} T(e) \quad & \mbox{see Definition~\ref{BasisDef}} \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(e) & \mbox{since $e$ is equaliser} \\
& = &
T(e) \\
& = &
T(e) \mathrel{\circ} \idmap.
\end{array}$$
\end{iteMize}

\noindent Hence the homomorphism of algebras $a \mathrel{\circ} T(e)$, from
$F(X_{b}) = \mu_{X_{b}}$ to $a$ is an isomorphism. In particular,
$b'\colon X\rightarrow T(X_{b})$ in~(\ref{RestrictedBaseDiag}) is a
map of algebras, as inverse of an isomorphism of algebras. It is not
hard to see that it is also an isomorphism between the coalgebras
$b\colon X\rightarrow T(X)$ and $T(\eta) \colon T(X_{b}) \rightarrow
T^{2}(X_{b})$, as in Lemma~\ref{FreeAlgCoalgLem}. \qed

\auxproof{
We include the split equaliser argument in \Cat{Sets}\xspace,
  following~\cite[Lemma~6.5]{Mesablishvili06}.
Consider a diagram:
$$\vcenter{\xymatrix{
X\ar[r]^-{h} & Y\ar@<+1ex>[r]^-{f}\ar@<-1ex>[r]_-{g} & Z
}}\eqno{(*)}$$

\noindent It is called a \textit{split equaliser} if there are maps
$k\colon Z\rightarrow Y$ and $\ell\colon Y\rightarrow X$ with
$$\ell \mathrel{\circ} h = \idmap
\qquad
k \mathrel{\circ} f = \idmap
\qquad
k\mathrel{\circ} g = h \mathrel{\circ} \ell.$$

\noindent Such a split equaliser is indeed an equaliser:
\begin{iteMize}{$\bullet$}
\item if $h'\colon X'\rightarrow Y$ satisfies $f \mathrel{\circ} h' = g \mathrel{\circ}
  h'$, then $e = \ell \mathrel{\circ} h'\colon X'\rightarrow X$ satisfies: $h
  \mathrel{\circ} e = h \mathrel{\circ} \ell \mathrel{\circ} h' = k \mathrel{\circ} g \mathrel{\circ} h' = k \mathrel{\circ}
  f \mathrel{\circ} h' = \idmap \mathrel{\circ} h' = h'$.

\item if also $d\colon X'\rightarrow X$ satisfies $h \mathrel{\circ} d = h'$,
then $e = \ell \mathrel{\circ} h' = \ell \mathrel{\circ} h \mathrel{\circ} d = \idmap \mathrel{\circ} d = d.$
\end{iteMize}

\noindent Clearly, split equalisers are preserved under functor
application, and are thus absolute.

Now assume in~$(*)$ that $X\neq \emptyset$, $h$ is mono and satisfies
$f \mathrel{\circ} h = g \mathrel{\circ} h$, and that $f,g$ form a coreflexive pair, via
$s\colon Z\rightarrow Y$ satisfying $s \mathrel{\circ} f = \idmap = s \mathrel{\circ}
g$. Thus we can form the cokernel pair $q_{1},q_{2}\colon
Y\rightrightarrows D$ of $h$ as pushout:
$$\xymatrix@R-1pc{
X\ar[r]^-{h}\ar[d]_{h} & Y\ar[d]^{q_2}\ar@/^2ex/[ddr]^{g} \\
Y\ar[r]_-{q_1}\ar@/_2ex/[drr]_{f} & D\pullback[lu]\ar@{-->}[dr]^-{r} \\
& & Z
}$$

\noindent The first claim is that this induced map $r$ is injective.
We can construct $D$ explicitly as $Y+Y/\!\equiv$, where $\equiv$ is
the least equivalence relation on $Y+Y$ containing the pairs
$\tuple{\kappa_{1}h(x), \kappa_{2}h(x)}$, for $x\in X$. Thus,
$\equiv$ contains the following elements:
\begin{iteMize}{$\bullet$}
\item $\tuple{\kappa_{1}y, \kappa_{1}y}$, for $y\in Y$;
\item $\tuple{\kappa_{2}y, \kappa_{2}y}$, for $y\in Y$;
\item $\tuple{\kappa_{1}h(x), \kappa_{2}h(x)}$, for $x\in X$;
\item $\tuple{\kappa_{2}h(x), \kappa_{1}h(x)}$, for $x\in X$.
\end{iteMize}

\noindent Reflexivity and symmetry are obvious, by construction.  For
transitivity, assume we have pairs $\tuple{\kappa_{1}h(x),
  \kappa_{2}h(x)}$ and $\tuple{\kappa_{2}h(x'), \kappa_{1}h(x')}$,
where $h(x) = h(x')$. The composed pair $\tuple{\kappa_{1}h(x),
  \kappa_{1}h(x')}$ is then also covered by the abover description,
namely by the first item.

An element $[w]$ of $Y+Y/\!\equiv$ is thus of the form:
\begin{iteMize}{$\bullet$}
\item $[w] = \{\kappa_{1}h(x), \kappa_{2}h(x)\}$, in which case
$r([w]) = f(h(x)) = g(h(x))$, and thus $(s \mathrel{\circ} r)([w]) = h(x)$;
\item $[w] = \{\kappa_{1}y\}$, where $y\neq h(x)$, and then $r([w]) =
  f(y)$, and thus $(s \mathrel{\circ} r)([w]) = y$;
\item $[w] = \{\kappa_{2}y\}$, where $y\neq h(x)$, and then $r([w]) =
  g(y)$, and thus $(s \mathrel{\circ} r)([w]) = y$.
\end{iteMize}

\noindent If $r([w]) = r([w'])$, then by applying $s\colon
Z\rightarrow Y$, we see:
\begin{iteMize}
\item if $[w] = \{\kappa_{1}h(x), \kappa_{2}h(x)\}$, then the second
and third cases cannot occur for $w'$, so $[w'] = \{\kappa_{1}h(x'),
\kappa_{2}h(x')\}$ for some $x'$. But then $h(x) = h(x')$, and
so $[w]=[w']$.

\item if $[w] = \{\kappa_{1}y\}$ with $y\neq h(x)$, the first case for
  $[w']$ cannot occur; the second case immediatly yields $[w] = [w']$,
  so we concentrate on the third: if $[w'] = \{\kappa_{2}y'\}$, then
  $f(y) = g(y')$, and thus $y = y'$. Now we use that $h$ is the
  equaliser of $f,g$, so that there is an $x$ with $h(x) \neq y$.  But
  this is impossible.

\item The case $[w] = \{\kappa_{2}y\}$ is handled similarly.
\end{iteMize}

Since $X\neq\emptyset$ and $h\colon X\rightarrow Y$ is injective (as
equaliser) there is a section $i\colon Y\rightarrow X$ with $i \mathrel{\circ}
h = \idmap$, making $h$ a split mono. Also, $D\neq \emptyset$, so that
there is an $r'\colon Z\rightarrow D$ with $r' \mathrel{\circ} r = \idmap$,
using that $r$ is injective. We know form a map $j$ in:
$$\xymatrix@R-1pc{
X\ar[r]^-{h}\ar[d]_{h} & Y\ar[d]^{q_2}\ar@/^2ex/[ddr]^{h \mathrel{\circ} i} \\
Y\ar[r]_-{q_1}\ar@/_2ex/[drr]_{\idmap} & D\pullback[lu]\ar@{-->}[dr]^-{j} \\
& & Y
}$$

\noindent By construction, this pair $i\colon Y\rightarrow X, j\colon
D\rightarrow Y$ makes $h\colon X\rightarrowtail Y \rightrightarrows D$
a split equaliser.

In a next step $i\colon Y\rightarrow X, j\mathrel{\circ} r'\colon Z\rightarrow
Y$ makes $(*)$ a split equaliser, since $j \mathrel{\circ} r' \mathrel{\circ} f
= j \mathrel{\circ} r' \mathrel{\circ} r \mathrel{\circ} q_{1} = j \mathrel{\circ} q_{1} = \idmap$ and
$j \mathrel{\circ} r' \mathrel{\circ} g = j \mathrel{\circ} r' \mathrel{\circ} r \mathrel{\circ} q_{2} = j \mathrel{\circ}
q_{2} = h \mathrel{\circ} i$.

\medskip

Finally we also check that $\varphi = a \mathrel{\circ} T(e) \colon T(B)
\congrightarrow X$ is a map of coalgebras, in:
$$\xymatrix@R-1pc{
T^{2}(B)\ar[rr]^-{T(\varphi)}_-{\cong} & & T(X) \\
T(B)\ar[u]^{T(\eta)}\ar[rr]^-{\varphi}_-{\cong} & & X\ar[u]_{b}
}$$

\noindent This is simple:
$$\begin{array}{rcl}
b \mathrel{\circ} \varphi
& = &
b \mathrel{\circ} a \mathrel{\circ} T(e) \\
& = &
\mu \mathrel{\circ} T(b) \mathrel{\circ} T(e) \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(e) \\
& = &
T(e) \\
& = &
T(a) \mathrel{\circ} T(\eta) \mathrel{\circ} T(e) \\
& = &
T(a) \mathrel{\circ} T^{2}(e) \mathrel{\circ} T(\eta) \\
& = &
T(\varphi) \mathrel{\circ} T(\eta).
\end{array}$$
}
\end{myproof}

\subsection{Complete lattices}\label{CompleteLatticeSubsec}

Consider the powerset monad $\powerset$ on \Cat{Sets}\xspace, with the category
$\Cat{CL} = \textsl{Alg}\xspace(\powerset)$ of complete lattices and join-preserving maps
as its category of algebras.  The induced comonad
$\smash{\overline{\powerset}} \colon \Cat{CL} \rightarrow \Cat{CL}$ as
in~(\ref{ComonadFromMonadDiag}) sends a complete lattice $(L,\leq)$ to
the lattice $(\powerset(L), \subseteq)$ of subsets, ignoring the original
order $\leq$.  The counit $\varepsilon \colon
\smash{\overline{\powerset}(L)} \rightarrow L$ sends a subset $U\in\powerset(L)$
to its join $\varepsilon(U) = \bigvee U$; the comultiplication $\delta
\colon {\overline{\powerset}(L)} \rightarrow
\smash{\overline{\powerset}^{2}(L)}$ sends $U\in\powerset(L)$ to the subset of
singletons $\delta(U) = \set{\{x\}}{x\in U}$.

An (Eilenberg-Moore) coalgebra of the comonad
$\smash{\overline{\powerset}}$ on $\Cat{CL}$ is a map $b\colon L
\rightarrow \smash{\overline{\powerset}(L)}$ in $\Cat{CL}$ satisfying
$\varepsilon \mathrel{\circ} b = \idmap$ and $\delta \mathrel{\circ} b =
\overline{\powerset}(b) \mathrel{\circ} b$. More concretely, this says that $\bigvee
b(x) = x$ and $\set{\{y\}}{y\in b(x)} = \set{b(y)}{y\in b(x)}$. It is
shown in~\cite{Jacobs94b} that a complete lattice $L$ carries
such a coalgebra structure $b$ if and only if $L$ is \emph{atomic},
where:
$$\begin{array}{rcl}
b(x)
& = &
\setin{a}{L}{a \mbox{ is an atom with }a \leq x}.
\end{array}$$

\noindent Thus, such a coalgebra of the comonad
$\smash{\overline{\powerset}}$, if it exists, is uniquely determined and
gives a decomposition of lattice elements into the atoms below it. The
atoms in the lattice thus form a basis.

(Recall: the complete lattice $L$ is atomic when each element is the
join of the atoms below it. And an atom $a\in L$ is a non-zero element
with no non-zero elements below it, satisfying: $a \leq \bigvee U$
implies $a \leq x$ for some $x\in U$.)

The equaliser~(\ref{BasisEqualiserDiag}) for the basic elements in
this situation, for an atomic complete lattice $L$, is the set of
atoms:
$$X_{b}
=
\setin{x}{L}{\{x\} = b(x)}
=
\setin{x}{L}{x\mbox{ is an atom}}.$$

\noindent If $X_{b}\neq \emptyset$, the induced map $\powerset(X_{b})
\rightarrow L$ is an isomorphism, by Lemma~\ref{SetsBasisProp}.

\subsection{Vector spaces}\label{VectorSpaceSubsec}

For a semiring $S$ one can define the multiset monad $\ensuremath{\mathcal{M}}_{S}$ on
$\Cat{Sets}\xspace$ by $\ensuremath{\mathcal{M}}_{S}(X) = \set{\varphi\colon X\rightarrow
  S}{\ensuremath{\mathrm{supp}}(\varphi)\mbox{ is finite}}$. Such an element $\varphi$
can be identified with a formal finite sum $\sum_{i}s_{i}x_{i}$ with
multiplicities $s_{i}\in S$ for elements $x_{i}\in X$. The unit of
this monad $\eta\colon X \rightarrow \ensuremath{\mathcal{M}}_{S}(X)$ is given by
singleton multisets: $\eta(x) = 1x$. The multiplication $\mu \colon
\ensuremath{\mathcal{M}}_{S}^{2}(X) \rightarrow \ensuremath{\mathcal{M}}_{S}(X)$ involves (matrix)
multiplication: $\mu(\sum_{i}s_{i}\varphi_{i})(x) = \sum_{i}
s_{i}\cdot \varphi_{i}(x)$, where $\cdot$ is the multiplication of the
semiring $S$.

The category of algebras $\textsl{Alg}\xspace(\ensuremath{\mathcal{M}}_{S})$ of the multiset monad
$\ensuremath{\mathcal{M}}_S$ is the category of $\Cat{Mod}_S$ of modules over $S$:
commutative monoids with $S$-scalar multiplication, see
\textit{e.g.}~\cite{CoumansJ13} for more information. The induced
comonad $\overline{\ensuremath{\mathcal{M}}_S} \colon \Cat{Mod}_{S} \rightarrow
\Cat{Mod}_{S}$ from~(\ref{ComonadFromMonadDiag}) sends such a module
$X = (X, +, 0, \mathrel{\bullet})$ to the free module $\ensuremath{\mathcal{M}}_{S}(X)$ of finite
multisets (formal sums) on the underlying set $X$, ignoring the
existing module structure on $X$. The counit and comultiplication are
given by:
\begin{equation}
\label{MltComonadStructDiag}
\vcenter{\xymatrix@R-2pc{
X & & \ensuremath{\mathcal{M}}_{S}(X)\ar[ll]_-{\varepsilon}\ar[rr]^-{\delta} & & \ensuremath{\mathcal{M}}_{S}^{2}(X) \\
\big(\sum_{j} s_{j}\mathrel{\bullet} x_{j}\big)  & &
   \big(\sum_{j}s_{j}x_{j}\big)\ar@{|->}[ll]\ar@{|->}[rr] & &
   \big(\sum_{j}s_{j}(1x_{j})\big).
}}
\end{equation}

\noindent The formal sum (multiset) in the middle is mapped by the
counit $\varepsilon$ to an actual sum in $X$, namely to its
interpretation.  The comultiplication $\delta$ maps this formal sum to
a multiset of multisets, with the inner multisets given by singletons
$1x_{j} = \eta(x_{j})$.

The following is a novel observation, motivating the view of
coalgebras on algebras as bases.

\begin{thm}
\label{OperatorCoalgThm}
Let $X$ be a vector space, say over $S=\mathbb{R}$ or $S=\mathbb{C}$.
Coalgebras $X\rightarrow \overline{\ensuremath{\mathcal{M}}_{S}}(X)$ correspond to (Hamel)
bases on $X$.
\end{thm}

\begin{myproof}
Suppose we have a basis $B\subseteq X$ for the vector space $X$. Then
we can define a coalgebra $\smash{b \colon X\rightarrow
  \overline{\ensuremath{\mathcal{M}}_{S}}(X)}$ via (finite) formal sums $b(x) =
\sum_{j}s_{j}a_{j}$, where $s_{j}\in S$ is the $j$-th coefficient of
$x$ wrt\ $a_{j}\in B\subseteq X$.  By construction we have
$\varepsilon \mathrel{\circ} b = \idmap$. The equation $\delta \mathrel{\circ} b =
\ensuremath{\mathcal{M}}_{S}(b) \mathrel{\circ} b$ holds because $b(a) = 1a$, for basic elements
$a\in B$.

Conversely, given a coalgebra $\smash{b \colon X\rightarrow
  \overline{\ensuremath{\mathcal{M}}_{S}}(X)}$ take $X_{b} = \setin{a}{X}{b(a) = 1a}$ as
in~(\ref{BasisEqualiserDiag}). Any finite subset of elements of
$X_{b}$ is linearly independent: if $\sum_{j}s_{j}\mathrel{\bullet} a_{j} = 0$,
for finitely many $a_{j}\in X_{b}$, then in $\ensuremath{\mathcal{M}}_{S}(X)$,
$$\textstyle 0
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
b(0)
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
b(\sum_{j}s_{j}\mathrel{\bullet} a_{j})
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
\sum_{j}s_{j}b(a_{j})
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
\sum_{j}s_{j}(1a_{j})
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
\sum_{j}s_{j}a_{j}.$$

\noindent Hence $s_{j} = 0$, for each $j$. Next, since $\delta \mathrel{\circ}
b = \ensuremath{\mathcal{M}}_{S}(b) \mathrel{\circ} b$, each $a_{j}$ in $b(x) = \sum_{j}s_{j}a_{j}$
satisfies $b(a_{j}) = 1a_{j}$, so that $a_{j} \in X_{b}$. Because
$\varepsilon \mathrel{\circ} b = \idmap$, each element $x\in X$ can be
expressed as sum of such basic elements. \qed
\end{myproof}

A basis for complete lattices in
Subsection~\ref{CompleteLatticeSubsec}, if it exists, is uniquely
determined. In the context of vector spaces bases are unique up to
isomorphism.

Our next example involves convex sets, where extreme points play the
role of base vectors. Via the language of coalgebras we can make the
similarity with vector spaces explicit.

\subsection{Convex sets}\label{ConvexSubsec}

The (discrete probability) distribution monad $\ensuremath{\mathcal{D}}$ on $\Cat{Sets}\xspace$ is
given by $\ensuremath{\mathcal{D}}(X) = \set{\varphi\colon X \rightarrow [0,1]}{
  \ensuremath{\mathrm{supp}}(\varphi) \mbox{ is finite, and } \sum_{x\in X}\varphi(x) =
  1}$.  The unit and multiplication of this monad are as for the
multiset monad $\ensuremath{\mathcal{M}}_S$, described above.

Algebras of the distribution monad can be identified with ``convex
sets'' (see \textit{e.g.}~\cite{Jacobs10e}), where convex sums exist:
the mapping $\ensuremath{\mathcal{D}}(X) \rightarrow X$ sends a formal convex combination
to an actual convex sum. A typical example is the unit interval
$[0,1]$. Notice that it does not have arbitrary sums; but convex sums
exist in $[0,1]$.  An algebra homomorphism preserves such convex
sums. Such a map is usually called `affine'. We write $\Cat{Conv}$ for
this category $\textsl{Alg}\xspace(\ensuremath{\mathcal{D}})$ of convex sets and affine maps.

A point $x\in X$ in a convex set $X$ is called \textit{extreme} if it
does not occur as non-trivial convex combination: if $x =
\sum_{i}r_{i}x_{i}$, then $r_{j}=1$ and $x_{j}=x$, for some $j$, and
thus $r_{i}=0$ for $i\neq j$. One usually writes $\partial X \subseteq
X$ for the subset of extreme points. In a free convex set $\ensuremath{\mathcal{D}}(Y)$,
for a set $Y$, the extreme points are the singletons $\eta(y) = 1y$,
for $y\in Y$. Thus $\partial\ensuremath{\mathcal{D}}(X) \cong X$.

Now assume we have a coalgebra $\smash{b\colon X \rightarrow
  \overline{\ensuremath{\mathcal{D}}}(X)}$ for the induced comonad $\overline{\ensuremath{\mathcal{D}}}
\colon \Cat{Conv} \rightarrow \Cat{Conv}$. We form the subset $X_{b} =
\setin{x}{X}{b(x) = 1x}$ as in~(\ref{BasisEqualiserDiag}), and claim
$X_{b} = \partial X$, that is, these basic elements in $X_{b}$ are
precisely the extreme points.

It is easy to see that there is an inclusion $\partial X \subseteq
X_{b}$: if $x$ is extreme, and $b(x)$ is a formal sum
$\sum_{i}r_{i}x_{i}$, then $x$ equals the actual sum
$\sum_{i}r_{i}x_{i}\in X$. But then $r_{j} = 1$ and $x = x_{j}$, for
some $j$ --- and $r_{i}=0$ for $i\neq j$. Hence $b(x) = 1x_{j} = 1x$.

For the reverse inclusion $X_{b} \subseteq \partial X$, assume $x\in
X$ satisfies $b(x) = 1x$, and $x = \sum_{i}r_{i}x_{i}$, where $r_{i}
\neq 0$ and $\sum_{i}r_{i}=1$. Since $b$ is an algebra homomorphism,
it preserves convex sums:
$$\begin{array}{rcccccccl}
1
& = &
(1x)(x)
& = &
b(x)(x)
& = &
b(\sum_{i}r_{i}x_{i})(x)
& = &
\sum_{i}r_{i}b(x_{i})(x).
\end{array}$$

\noindent But then $b(x_{i})(x)=1$, and so $x_{i} = x$ for each $i$.
Hence $x = \sum_{i}r_{i}x_{i}$ is a singleton sum, making $x$ extreme.

We thus see that a $\smash{\overline{\ensuremath{\mathcal{D}}}}$-coalgebra $b\colon X
\rightarrow \ensuremath{\mathcal{D}}(X)$ determines a coalgebra $b'\colon X \rightarrow
\ensuremath{\mathcal{D}}(\partial X)$, as in~(\ref{RestrictedBaseDiag}), that describes
each element as convex sum of extreme points. As we have seen, this
map $b'$ is an isomorphism $\smash{X \conglongrightarrow
  \ensuremath{\mathcal{D}}(\partial X)}$ describing each convex set with a basis as a
free convex set on its extreme points. This is the essence of the
equivalence of categories $\textsl{CoAlg}\xspace(\overline{\ensuremath{\mathcal{D}}}) \simeq \Cat{Sets}\xspace$.

The situation is reminiscent of the Krein-Milman theorem, which states
that a convex and compact subset $S$ of a locally convex space is
equal to the closed convex hull of its extreme points: $S =
\overline{\ensuremath{\mathcal{D}}(\partial S)}$, where $\overline{(-)}$ is the closure
operation. What we have here is a non-topological version of such a
result.

\section{Order-theoretic examples}\label{OrderSec}

Assume $\cat{A}$ is a poset-enriched category. This means that all
homsets $\cat{A}(X,Y)$ are posets, and that pre- and post-composition
are monotone. In this context maps $f\colon X\rightarrow Y$ and
$g\colon Y\rightarrow X$ in opposite direction form an adjunction
$f\dashv g$ (or Galois connection) if there are inequalities
$\idmap[X] \leq g\mathrel{\circ} f$ and $f\mathrel{\circ} g \leq \idmap[Y]$,
corresponding to unit and counit of the adjunction. In such a
situation the adjoints $f,g$ determine each other.

A monad $T = (T, \eta, \mu)$ on such a poset-enriched category
$\cat{A}$ is said to be of \textit{Kock-Z{\"o}berlein type} or just a
\textit{Kock-Z{\"o}berlein monad} if $T\colon \cat{A}(X,Y)
\rightarrow \cat{A}(TX,TY)$ is monotone and $T(\eta_{X}) \leq
\eta_{TX}$ holds in the homset $\cat{A}\big(T(X), T^{2}(X)\big)$. This
notion is introduced in~\cite{Kock95} in proper 2-categorical form.
Here we shall use the special `poset' instance---like
in~\cite{Escardo98} where the dual form occurs. The following result
goes back to~\cite{Kock95}; for convenience we include the proof.

\begin{thm}
\label{KZAlgThm}
Let $T$ be a Kock-Z{\"o}berlein monad on a poset-enriched category
$\cat{A}$. For a map $a\colon T(X)\rightarrow X$ in $\cat{A}$ the
following statements are equivalent.
\begin{enumerate}[\em(1)]
\item $a\colon T(X)\rightarrow X$ is an (Eilenberg-Moore) algebra
of the monad $T$;

\item $a\colon T(X)\rightarrow X$ is a left-adjoint-left-inverse of the
  unit $\eta\colon X\rightarrow T(X)$; this means that $a\dashv
  \eta_{X}$ is a reflection.
\end{enumerate}
\end{thm}

\begin{myproof}
First assume $a\colon T(X)\rightarrow X$ is an algebra,
\textit{i.e.}~satisfies $a\mathrel{\circ} \eta = \idmap$ and $a \mathrel{\circ} \mu = a
\mathrel{\circ} T(a)$. It suffices to prove $\idmap \leq \eta \mathrel{\circ} a$,
corresponding to the unit of the reflection, since the equation
$a\mathrel{\circ} \eta = \idmap$ is the counit (isomorphism). This is easy, by
naturality: $\eta \mathrel{\circ} a = T(a) \mathrel{\circ} \eta \geq T(a) \mathrel{\circ} T(\eta)
= \idmap$.

In the other direction, assume $a\colon T(X)\rightarrow X$ is
left-adjoint-left-inverse of the unit $\eta\colon X\rightarrow T(X)$,
so that $a\mathrel{\circ}\eta = \idmap$ and $\idmap \leq \eta \mathrel{\circ} a$. We
have to prove $a \mathrel{\circ} \mu = a \mathrel{\circ} T(a)$. In one direction, we
have:
\begin{equation}
\label{KZMuEqn}
\begin{array}{rcl}
\mu
& \leq &
T(a),
\end{array}
\end{equation}

\noindent since $\mu \leq \mu \mathrel{\circ} T(\eta \mathrel{\circ} a) = T(a)$, and
thus $a \mathrel{\circ} \mu \leq a \mathrel{\circ} T(a)$. For the reverse inequality we
use:
$$\begin{array}[b]{rcll}
a \mathrel{\circ} T(a)
\hspace*{\arraycolsep}=\hspace*{\arraycolsep}
a \mathrel{\circ} T(a) \mathrel{\circ} T(\idmap)
& = &
a \mathrel{\circ} T(a) \mathrel{\circ} T(\mu) \mathrel{\circ} T(\eta) \\
& \leq &
a \mathrel{\circ} T(a) \mathrel{\circ} T(\mu) \mathrel{\circ} \eta \qquad
   & \mbox{since }T(\eta) \leq \eta \\
& = &
a \mathrel{\circ} \eta \mathrel{\circ} a \mathrel{\circ} \mu
   & \mbox{by naturality} \\
& = &
a\mathrel{\circ} \mu.
\end{array}\eqno{\qEd}$$
\end{myproof}

In a next step we consider the induced comonad $\overline{T}$ on the
category $\textsl{Alg}\xspace(T)$ of algebra of a Kock-Z{\"o}berlein monad $T$, as
in~\eqref{MonadIterDiag}. A first, trivial but important, observation
is that the category $\textsl{Alg}\xspace(T)$ is also poset enriched. It is not hard
to see that the comonad $\overline{T}$ is also of Kock-Z{\"o}berlein
type, in the sense that for each algebra
$\smash{(TX\stackrel{a}{\rightarrow} X)}$ we have:
$$\varepsilon_{\overline{T}(a)}
=
\mu
\leq
T(a)
=
\overline{T}(\varepsilon_{a})$$

\noindent by~(\ref{KZMuEqn}). Thus one may expect a result similar to
Theorem~\ref{KZAlgThm} for coalgebras of this comonad
$\overline{T}$. It is formulated in~\cite[Thm.~4.2]{Kock95} (and
attributed to the present author). We repeat the poset version in the
current context.

\begin{thm}
\label{KZCoAlgThm}
Let $T$ be a Kock-Z{\"o}berlein monad on a poset-enriched category
$\cat{A}$, with induced comonad $\overline{T}$ on the category of
algebras $\textsl{Alg}\xspace(T)$. Assume an algebra $a\colon T(X)\rightarrow X$. For
a map $c\colon X\rightarrow T(X)$, forming a map of algebras in,
\begin{equation}
\label{KZCoAlgEqn}
\vcenter{\xymatrix@C-.5pc{
\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}\ar[rr]^-{c}
& &
\overline{T}\ensuremath{\left(\xy
(0,4)*{TX};
(0,-4)*{X};
{\ar^{a} (0,2); (0,-2)};
\endxy\right)}
=
\ensuremath{\left(\xy
(0,4)*{T^{2}X};
(0,-4)*{TX};
{\ar^{\mu\rlap{$\scriptscriptstyle{_X}$}} (0,2); (0,-2)};
\endxy\right)}
}}
\end{equation}

\noindent the following statements are equivalent.
\begin{enumerate}[\em(1)]
\item $c\colon a\rightarrow \overline{T}(a)$ is an
  (Eilenberg-Moore) coalgebra of the comonad $\overline{T}$;

\item $c\colon a\rightarrow \overline{T}(a)$ is a
  left-adjoint-right-inverse of the counit $a\colon
  \overline{T}(a)\rightarrow a$; this means that $c\dashv
  a$ is a coreflection.
\end{enumerate}
\end{thm}

\begin{myproof}
Assume $c$ is a $\overline{T}$-coalgebra, \textit{i.e.}~$c \mathrel{\circ} a =
\mu \mathrel{\circ} T(c)$, $a \mathrel{\circ} c = \idmap$ and $T(\eta) \mathrel{\circ} c = T(c)
\mathrel{\circ} c$, like in Definition~\ref{BasisDef}. We have to prove $c
\mathrel{\circ} a \leq \idmap$, which is obtained in:
$$c \mathrel{\circ} a
=
\mu \mathrel{\circ} T(c)
\;\stackrel{(\ref{KZMuEqn})}{\leq}\;
T(a) \mathrel{\circ} T(c)
=
\idmap.$$

\noindent Conversely, assume a coreflection $c\dashv a$, so that $a
\mathrel{\circ} c = \idmap$ and $c \mathrel{\circ} a \leq \idmap$. We have to prove
$T(\eta) \mathrel{\circ} c = T(c) \mathrel{\circ} c$. In one direction we have $T(c)
\leq T(\eta \mathrel{\circ} a) \mathrel{\circ} T(c) = T(\eta)$, and thus $T(c) \mathrel{\circ} c
\leq T(\eta) \mathrel{\circ} c$.  In the other direction, we use:
$$\begin{array}[b]{rcll}
T(c) \mathrel{\circ} c
\hspace*{\arraycolsep}=\hspace*{\arraycolsep}
T^{2}(\idmap) \mathrel{\circ} T(c) \mathrel{\circ} c
& = &
T^{2}(a \mathrel{\circ} \eta) \mathrel{\circ} T(c) \mathrel{\circ} c \\
& \leq &
T^{2}(a) \mathrel{\circ} T(\eta) \mathrel{\circ} T(c) \mathrel{\circ} c \quad
   & \mbox{since }\rlap{$T(\eta) \leq \eta$} \\
& = &
T^{2}(a) \mathrel{\circ} T^{2}(c) \mathrel{\circ} T(\eta) \mathrel{\circ} c
   & \mbox{by naturality} \\
& = &
T(\eta) \mathrel{\circ} c.
\end{array}\eqno{\qEd}$$\vspace{3 pt}
\end{myproof}

\noindent One can iterate the $\overline{(-)}$ construction, as
in~\eqref{MonadIterDiag}. Below we show that for Kock-Z{\"o}berlein
monads the iteration stops after 3 steps. First we need another
characterisation. The proof is as before.

\begin{lem}
\label{KZAlgCoAlgLem}
Let $T$ be a Kock-Z{\"o}berlein monad on a poset-enriched category
$\cat{A}$, giving rise to comonad $\smash{\overline{T}}$ on $\textsl{Alg}\xspace(T)$
and monad $\smash{\overline{\overline{T}}}$ on
$\textsl{CoAlg}\xspace(\smash{\overline{T}})$. Assume:
\begin{iteMize}{$\bullet$}
\item an algebra $a\colon T(X)\rightarrow X$ in $\textsl{Alg}\xspace(T)$;
\item a coalgebra $c\colon X\rightarrow T(X)$ on $a$ in
  $\smash{\textsl{CoAlg}\xspace(\overline{T})}$;
\item an algebra $b\colon T(X)\rightarrow X$ on $c$ in
  $\smash{\textsl{Alg}\xspace(\overline{\overline{T}})}$, where:
\begin{iteMize}{$-$}
\item $b \mathrel{\circ} c = \idmap$ and $b \mathrel{\circ} T(b) = b \mathrel{\circ} T(a)$,
since $b$ is a $\smash{\overline{\overline{T}}}$-algebra;

\item $a \mathrel{\circ} T(b) = b \mathrel{\circ} \mu$, since $b$ is a map of algebras
$\smash{a \rightarrow \overline{T}(a) = \mu}$;

\item $c \mathrel{\circ} b = T(b) \mathrel{\circ} T(\eta)$, since $b$ is a map of
algebras $\smash{\delta = \overline{\overline{c}} \rightarrow c}$.
\end{iteMize}
\end{iteMize}

\noindent The following statements are then equivalent.
\begin{enumerate}[\em(1)]
\item $\smash{b\colon \overline{\overline{T}}(c)\rightarrow c}$ is an
  algebra of the monad $\smash{\overline{\overline{T}}}$;

\item $\smash{b\colon \overline{\overline{T}}(c)\rightarrow c}$ is a
  left-adjoint-left-inverse of the unit $\smash{c\colon c \rightarrow
  \overline{\overline{T}}(c)}$. \qed
\end{enumerate}
\end{lem}

\auxproof{
First assume $b\colon T(X) \rightarrow X$ is a
$\smash{\overline{\overline{T}}}$-algebra. We have to show that there is a
reflection $b\dashv c$, \textit{i.e.}~that $b \mathrel{\circ} c = \idmap$ and
$\idmap \leq c \mathrel{\circ} b$. The former holds by assumption, and the
latter holds because:
$$\begin{array}{rcll}
c \mathrel{\circ} b
& = &
T(b) \mathrel{\circ} T(\eta)
   & \mbox{since $b$ is a map of coalgebras} \\
& \geq &
T(b) \mathrel{\circ} T(c)
   & \mbox{since $T(c) \leq T(\eta)$, see the proof of
    Theorem~\ref{KZCoAlgThm}} \\
& = &
\idmap
\end{array}$$

In the other direction, assume $b$ is a map of algebras
$\overline{T}(c) \rightarrow c$ with a reflection $b \dashv c$. We have
to show that $b$ is a $\smash{\overline{\overline{T}}}$-algebra,
\textit{i.e.}~satisfies $b \mathrel{\circ} c = \idmap$ and $b \mathrel{\circ} T(b) = b
\mathrel{\circ} T(a)$. Again, the former holds by assumption, and for the
latter we have $T(a) \leq T(b)$, since $T(b) \geq T(b) \mathrel{\circ} T(c
\mathrel{\circ} a) = T(a)$, and thus $b \mathrel{\circ} T(a) \leq b\mathrel{\circ} T(b)$. For the
reverse inequality we use:
$$\begin{array}{rcll}
b \mathrel{\circ} T(b)
& = &
b \mathrel{\circ} T(b) \mathrel{\circ} T^{2}(\idmap) \\
& = &
b \mathrel{\circ} T(b) \mathrel{\circ} T^{2}(a \mathrel{\circ} c) \\
& \leq &
b \mathrel{\circ} T(b) \mathrel{\circ} T^{2}(a) \mathrel{\circ} T(\eta)
   & \mbox{since $T(c) \leq T(\eta)$} \\
& \leq &
b \mathrel{\circ} T(b) \mathrel{\circ} T(\eta) \mathrel{\circ} T(a)
   & \mbox{by naturality} \\
& = &
b \mathrel{\circ} c \mathrel{\circ} b \mathrel{\circ} T(a)
   & \mbox{since $b$ is a map of algebras} \\
& = &
b \mathrel{\circ} T(a).
\end{array}$$
}

The next result shows how such series of adjunctions can arise.

\begin{lem}
\label{KZAlgCoAlgAlgLem}
Assume an algebra $a\colon T(X)\rightarrow X$ of a Kock-Z{\"o}berlein
monad. The free algebra $T(X)$ then carries multiple (co)reflections
(algebras and coalgebras) in a situation:
\begin{equation}
\label{KZAlgCoAlgAlgEqn}
\vcenter{\def\labelstyle{\scriptstyle}\xymatrix{
T^{2}(X)\ar@/_3ex/[d]_{\dashv\;}|{\mathstrut\mu}\ar@/_12ex/[d]_{T(a)} \\
T(X)\ar[u]^{\dashv}_{\eta}
   \ar@/^7.5ex/[u]^{\dashv\;\;\;}|{\mathstrut T(\eta)} \\
}}
\end{equation}

\noindent This yields a functor $T\colon \textsl{Alg}\xspace(T)
\rightarrow \smash{\textsl{Alg}\xspace(\overline{\overline{T}})}$ between categories of
algebras.
\end{lem}

\begin{myproof}
We check all (co)reflections from right to left.
\begin{iteMize}{$\bullet$}
\item In the first case the counit is the identity since $\mu \mathrel{\circ}
  \eta = \idmap$; because $T(\eta) \leq \eta$ for a Kock-Z{\"o}berlein
  monad, we get a unit $\eta \mathrel{\circ} \mu = T(\mu) \mathrel{\circ} \eta \geq
  T(\mu) \mathrel{\circ} T(\eta) = \idmap$. (This follows already from
  Theorem~\ref{KZAlgThm}.)

\item In the next case we have a coreflection $T(\eta) \dashv \mu$
  since the unit is the identity $\mu \mathrel{\circ} T(\eta) = \idmap$, and:
  $T(\eta) \mathrel{\circ} \mu = \mu \mathrel{\circ} T^{2}(\eta) \leq \mu \mathrel{\circ} T(\eta)
  = \idmap$.

\item Finally one gets a reflection $T(a) \dashv T(\eta)$ from the
  reflection $a\dashv\eta$ from Theorem~\ref{KZAlgThm}: $T(a) \mathrel{\circ}
  T(\eta) = T(a \mathrel{\circ} \eta) = \idmap$ and $T(\eta) \mathrel{\circ} T(a) =
  T(\eta \mathrel{\circ} a) \geq T(\idmap) = \idmap$. \qed
\end{iteMize}

\auxproof{
To be precise, we also have to check:
\begin{iteMize}{$\bullet$}
\item $T(\eta)$ is a map of algebras $\mu_{TX}\rightarrow\mu_{X}$;
this is obvious.

\item $T(a)$ is a map of coalgebras $T(\eta_{X}) \rightarrow
  T(\eta_{TX})$, and a map of algebras $\mu_{TX}\rightarrow\mu_{X}$;
  the latter is trivial, and for the former we use naturality:
  $T(\eta_{X}) \mathrel{\circ} T(a) = T^{2}(a) \mathrel{\circ} T(\eta_{TX})$.
\end{iteMize}

Additionally, if $f\colon X\rightarrow X'$ is a map of algebras
$a\rightarrow a'$ in $\textsl{Alg}\xspace(T)$, then $T(f)\colon T(X) \rightarrow
T(X')$ is a morphsm of algebras $T(a)\rightarrow T(a')$ in
$\smash{\textsl{Alg}\xspace(\overline{\overline{T}})}$. This is obvious.
}
\end{myproof}

\noindent This lemma describes the only form that such structures can have.
This is the main (new) result of this section.

\begin{thm}
\label{KZCoAlgBasisThm}
If we have a reflection-coreflection-reflection chain $b \dashv c
\dashv a \dashv \eta_{X}$ on an object $X$, like in
Lemma~\ref{KZAlgCoAlgLem}, then $X$ is a free algebra.

Thus: for a Kock-Z{\"o}berlein monad $T$, the functor $T\colon \textsl{Alg}\xspace(T)
\rightarrow \smash{\textsl{Alg}\xspace(\overline{\overline{T}})}$ is an equivalence of
categories.
\end{thm}

\begin{myproof}
Assume $b \dashv c \dashv a \dashv \eta_{X}$ on $X$, and consider the
equaliser~(\ref{BasisEqualiserDiag}) in:
\begin{equation}
\label{KZCoAlgBasisEqual}
\vcenter{\xymatrix@R-2pc@C-1pc{
X_{c}\ar@{ >->}[rr]^-{e} & & X
   \ar@<+.5ex>[rr]^-{c}\ar@<-.5ex>[rr]_-{\eta} & & T(X) \\
 & T(X)\ar[ur]_-{b} \\
X\ar[ur]_-{\eta}\ar@{-->}[uu]^{k}
}}
\end{equation}

\noindent We use the letter `$k$' because the elements in $X_c$ will
turn out to be compact elements, in the examples later on. The first
thing we note is:
\begin{equation}
\label{KZCoAlgBasisEqn}
\begin{array}{rcl}
k \mathrel{\circ} e
& = &
\idmap[X_c].
\end{array}
\end{equation}

\noindent This follows since $e$ is a mono, and:
$$\begin{array}{rcll}
e \mathrel{\circ} k \mathrel{\circ} e
& = &
b \mathrel{\circ} \eta \mathrel{\circ} e \qquad
  & \mbox{by construction of $k$} \\
& = &
b \mathrel{\circ} c \mathrel{\circ} e
   & \mbox{since $e$ is equaliser} \\
& = &
e & \mbox{since $b$ is a $\smash{\overline{\overline{T}}}$-algebra and
   $c$ is unit.}
\end{array}$$

Next we observe that the object $X_c$ carries a $T$-algebra structure
$a_c$ inherited from $a\colon T(X)\rightarrow X$, as in:
$$\xymatrix{
a_{c} \stackrel{\textrm{def}}{=} \Big(T(X_{c})\ar[r]^-{T(e)} &
   T(X)\ar[r]^-{a} & X\ar[r]^-{k} & X_{c}\Big)
}$$

\noindent It is an algebra indeed, since:
$$a_{c} \mathrel{\circ} \eta
=
k \mathrel{\circ} a \mathrel{\circ} T(e) \mathrel{\circ} \eta
=
k \mathrel{\circ} a \mathrel{\circ} \eta \mathrel{\circ} e
=
k \mathrel{\circ} e
\;\smash{\stackrel{(\ref{KZCoAlgBasisEqn})}{=}}\;
\idmap.$$

\noindent The other algebra equation is left to the reader.

\auxproof{
First we make explicit what it means for a map $b\colon
T(X)\rightarrow X$ in to be an algebra (on coalgebra $c$ on
algebra $a$):
\begin{iteMize}{$\bullet$}
\item $b \mathrel{\circ} c = \idmap$ and $b \mathrel{\circ} T(b) = b \mathrel{\circ} T(a)$,
since $b$ is a $\smash{\overline{\overline{T}}}$-algebra;

\item $a \mathrel{\circ} T(b) = b \mathrel{\circ} \mu$, since $b$ is a map of algebras
$\smash{a \rightarrow \overline{T}(a) = \mu}$;

\item $c \mathrel{\circ} b = T(b) \mathrel{\circ} T(\eta)$, since $b$ is a map of
algebras $\smash{\delta = \overline{\overline{c}} \rightarrow c}$.
\end{iteMize}

\noindent Now we use that the equaliser map $e$ is a mono in:
$$\begin{array}{rcll}
\lefteqn{e \mathrel{\circ} a_{c} \mathrel{\circ} T(a_{c})} \\
& = &
e \mathrel{\circ} k \mathrel{\circ} a \mathrel{\circ} T(e) \mathrel{\circ} T(k \mathrel{\circ} a \mathrel{\circ} T(e)) \\
& = &
b \mathrel{\circ} \eta \mathrel{\circ} a \mathrel{\circ} T(b \mathrel{\circ} \eta) \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e)
   \quad
  & \mbox{by~(\ref{KZCoAlgBasisEqual})} \\
& = &
b \mathrel{\circ} \eta \mathrel{\circ} b \mathrel{\circ} \mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(a)\mathrel{\circ} T^{2}(e)
   & \mbox{see the properties above} \\
& = &
b \mathrel{\circ} \eta \mathrel{\circ} b \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e) \\
& = &
b \mathrel{\circ} T(b) \mathrel{\circ} \eta \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e)
   & \mbox{by naturality} \\
& = &
b \mathrel{\circ} T(a) \mathrel{\circ} \eta \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e)
   & \mbox{see the properties above} \\
& = &
b \mathrel{\circ} \eta \mathrel{\circ} a \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e)
   & \mbox{by naturality} \\
& = &
e \mathrel{\circ} k \mathrel{\circ} a \mathrel{\circ} T(a) \mathrel{\circ} T^{2}(e)
  & \mbox{by~(\ref{KZCoAlgBasisEqual})} \\
& = &
e \mathrel{\circ} k \mathrel{\circ} a \mathrel{\circ} \mu \mathrel{\circ} T^{2}(e)
  & \mbox{since $a$ is a $T$-algebra} \\
& = &
e \mathrel{\circ} k \mathrel{\circ} a \mathrel{\circ} T(e) \mathrel{\circ} \mu
   & \mbox{by naturality} \\
& = &
e \mathrel{\circ} a_{c} \mathrel{\circ} \mu.
\end{array}$$
}

Next we show that the transpose $a\mathrel{\circ} T(e) \colon T(X_{c})
\rightarrow X$ of the equaliser $e\colon X_{c} \rightarrowtail X$ is
an isomorphism of algebras $\mu_{X_c} \cong a$. The inverse is $T(k)
\mathrel{\circ} c \colon X\rightarrow T(X)\rightarrow T(X_{c})$, since:
$$\begin{array}{rcll}
\lefteqn{\big(a\mathrel{\circ} T(e)\big) \mathrel{\circ} \big(T(k) \mathrel{\circ} c\big)} \\
& = &
a \mathrel{\circ} T(b \mathrel{\circ} \eta) \mathrel{\circ} c \qquad
  & \mbox{by~(\ref{KZCoAlgBasisEqual})} \\
& = &
b \mathrel{\circ} \mu \mathrel{\circ} T(\eta) \mathrel{\circ} c
   & \mbox{see the assumptions in Lemma~\ref{KZAlgCoAlgLem}} \\
& = &
b \mathrel{\circ} c \\
& = &
\idmap
   & \mbox{see Theorem~\ref{KZCoAlgThm}} \\
\lefteqn{\big(T(k) \mathrel{\circ} c\big) \mathrel{\circ} \big(a\mathrel{\circ} T(e)\big)} \\
& = &
T(k) \mathrel{\circ} \mu \mathrel{\circ} T(c) \mathrel{\circ} T(e) \quad
   & \mbox{since $c$ is a map
      $\smash{a \rightarrow \overline{T}(a) = \mu}$} \\
& = &
T(k) \mathrel{\circ} \mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(e)
   & \mbox{since $e$ is equaliser of $c$ and $\eta$} \\
& = &
T(k) \mathrel{\circ} T(e) \\
& = &
\idmap & \mbox{by~(\ref{KZCoAlgBasisEqn}).}
\end{array}$$
We continue to check that the assumed chain of adjunctions $b \dashv c
\dashv a \dashv \eta_{X}$ is related to the chain $T(a_{c}) \dashv
T(\eta) \dashv \mu \dashv \eta$ in~(\ref{KZAlgCoAlgAlgEqn}) via these
isomorphisms. In particular we still need to check that the
following two square commute.
$$\xymatrix@R1pc{
T^{2}(X_{c})\ar[rr]^-{T(a \mathrel{\circ} T(e))}_-{\cong} & & T(X)
& &
T^{2}(X_{c})\ar[d]_{T(a_{c})}\ar[rr]^-{T(a \mathrel{\circ} T(e))}_-{\cong} & &
   T(X)\ar[d]^{b} \\
T(X_{c})\ar[u]^{T(\eta)}\ar[rr]_-{a \mathrel{\circ} T(e)}^-{\cong} & & X\ar[u]_{c}
& &
T(X_{c})\ar[rr]_-{a \mathrel{\circ} T(e)}^-{\cong} & & X
}$$

\noindent These square commute since:
$$\begin{array}{rcll}
T(a \mathrel{\circ} T(e)) \mathrel{\circ} T(\eta)
& = &
T(a) \mathrel{\circ} T(\eta) \mathrel{\circ} T(e)
   & \mbox{by naturality} \\
& = &
T(e) \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(e) \\
& = &
\mu \mathrel{\circ} T(c) \mathrel{\circ} T(e) \\
& = &
c \mathrel{\circ} a \mathrel{\circ} T(e)
   & \mbox{see Theorem~\ref{KZCoAlgThm}} \\
a \mathrel{\circ} T(e) \mathrel{\circ} T(a_{c})
& = &
a \mathrel{\circ} T(e) \mathrel{\circ} T(k \mathrel{\circ} a \mathrel{\circ} T(e)) \\
& = &
a \mathrel{\circ} T(b \mathrel{\circ} \eta) \mathrel{\circ} T(a \mathrel{\circ} T(e))
  & \mbox{by~(\ref{KZCoAlgBasisEqual})} \\
& = &
b \mathrel{\circ} \mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(a \mathrel{\circ} T(e)) \quad
   & \mbox{see in Lemma~\ref{KZAlgCoAlgLem}} \\
& = &
b \mathrel{\circ} T(a \mathrel{\circ} T(e)).
\end{array}$$
We still have to check that the functor $T\colon \textsl{Alg}\xspace(T) \rightarrow
\smash{\textsl{Alg}\xspace(\overline{\overline{T}})}$ is an equivalence.  In the
reverse direction, given a coalgebra $c\colon
\overline{\overline{T}}(b) \rightarrow b$ on $X$, we take the induced
algebra $T(X_{c}) \rightarrow X_{c}$ on the
equaliser~(\ref{KZCoAlgBasisEqual}). Then $T(X_{c}) \congrightarrow X$
is an isomorphism of $\overline{\overline{T}}$-algebras, as we have
    seen.

For the isomorphism in the other direction, assume we start from an
algebra $a\colon T(X)\rightarrow X$, obtain the
$\overline{\overline{T}}$-algebra $T(a)$ described in the chain $T(a)
\dashv T(\eta) \dashv \mu \dashv \eta$ in~(\ref{KZAlgCoAlgAlgEqn}),
and then form the equaliser~(\ref{KZCoAlgBasisEqual}); it now looks as
follows.
$$\xymatrix@R-2pc@C-1pc{
X\ar@{ >->}[rr]^-{\eta_X} & & T(X)
   \ar@<+.5ex>[rr]^-{T(\eta)}\ar@<-.5ex>[rr]_-{\eta} & & T^{2}(X)
}$$

\noindent This is the equaliser requirement~\cite{Moggi88}, which
holds since $X$ carries an algebra structure. Clearly, $\eta \mathrel{\circ}
\eta = T(\eta) \mathrel{\circ} \eta$ by naturality. And if a map $f\colon
Y\rightarrow T(X)$ satisfies $\eta \mathrel{\circ} f = T(\eta) \mathrel{\circ} f$, then
$f$ factors through $\eta\colon X\rightarrow T(X)$ via $f' = a \mathrel{\circ}
f$, since
$$\eta \mathrel{\circ} f'
=
\eta \mathrel{\circ} a \mathrel{\circ} f
=
T(a) \mathrel{\circ} \eta \mathrel{\circ} f
=
T(a) \mathrel{\circ} T(\eta) \mathrel{\circ} f
=
f.$$

\noindent This $f'$ is unique with this property, since if $g\colon
Y\rightarrow X$ also satisfies $\eta \mathrel{\circ} g = f$, then $f' = a
\mathrel{\circ} f = a \mathrel{\circ} \eta \mathrel{\circ} g = g$. \qed
\end{myproof}

In the remainder of this section we review some examples.

\subsection{Dcpos over Posets}\label{DcpoSubsec}

The main example from~\cite{Jacobs94b} involves the ideal monad $\textsl{Idl}\xspace$
on the category \Cat{PoSets}\xspace of partially ordered sets with monotone
functions between them. In the light of Theorems~\ref{KZAlgThm}
and~\ref{KZCoAlgThm} we briefly review the essentials.

For a poset $X = (X,\leq)$ let $\textsl{Idl}\xspace(X)$ be the set of directed
downsets in $X$, ordered by inclusion. This $\textsl{Idl}\xspace$ is in fact a monad
on \Cat{PoSets}\xspace with unit $X\rightarrow\textsl{Idl}\xspace(X)$ given by principal downset
$x\mapsto\mathop{\downarrow}\! x$ and multiplication $\textsl{Idl}\xspace^{2}(X) \rightarrow
\textsl{Idl}\xspace(X)$ by union.  This monad is of Kock-Z{\"o}berlein type since for
$U\in\textsl{Idl}\xspace(X)$ we have:
$$\begin{array}{rcl}
\textsl{Idl}\xspace(\mathop{\downarrow}\!)(U)
\hspace*{\arraycolsep}=\hspace*{\arraycolsep}
\mathop{\downarrow}\!\set{\mathop{\downarrow}\! x}{x\in U}
& = &
\setin{V}{\textsl{Idl}\xspace(X)}{\exin{x}{U}{V\subseteq \mathop{\downarrow}\! x}} \\
& \subseteq &
\setin{V}{\textsl{Idl}\xspace(X)}{V\subseteq U} \qquad
    \mbox{since $U$ is a downset} \\
& = &
\mathop{\downarrow}\! U.
\end{array}$$

\auxproof{
For a poset $(X,\leq)$ a subset $U\subseteq X$ is called directed if
it is non-empty and for each pair $x_{1},x_{2}\in U$ there is a $y\in
U$ with $x_{1},x_{2}\leq y$. The set $\textsl{Idl}\xspace(X)$ contains the downclosed
directed subsets, ordered by inclusion. The mapping $X \mapsto
\textsl{Idl}\xspace(X)$ yields a functor $\Cat{PoSets}\xspace \rightarrow \Cat{PoSets}\xspace$: for $f\colon
X\rightarrow Y$ one defines $\textsl{Idl}\xspace(f)(U) = \mathop{\downarrow}\!\set{f(x)}{x\in U}$.
}

\noindent Applying Theorem~\ref{KZAlgThm} to the ideal monad yields the
(folklore) equivalence of the following points.
\begin{enumerate}[(1)]
\item $X$ is a directed complete partial order (dcpo): each directed
  subset $U\subseteq X$ has a join $\bigvee U$ in $X$;

\item The unit $\mathop{\downarrow}\!\; \colon  X \rightarrow  \textsl{Idl}\xspace(X)$
  has a left adjoint---which is the join;

\item $X$ carries a (necessarily unique) algebra structure $\textsl{Idl}\xspace(X)
  \rightarrow X$, which is also the join.
\end{enumerate}

\noindent Additionally, algebra maps are precisely the continuous
functions. Thus we may use as category $\Cat{Dcpo}\xspace = \textsl{Alg}\xspace(\textsl{Idl}\xspace)$.

The monad $\textsl{Idl}\xspace$ on $\Cat{PoSets}\xspace$ induces a comonad on $\Cat{Dcpo}\xspace$, written
$\overline{\textsl{Idl}\xspace}$, with counit $\varepsilon = \bigvee \colon \textsl{Idl}\xspace(X)
\rightarrow X$ and comultiplication $\delta = \textsl{Idl}\xspace(\mathop{\downarrow}\!) \colon
\textsl{Idl}\xspace(X)\rightarrow \textsl{Idl}\xspace^{2}(X)$, so that $\delta(U) =
\mathop{\downarrow}\!\set{\mathop{\downarrow}\! x}{x\in U}$. In order to characterise coalgebras
of this comonad $\overline{\textsl{Idl}\xspace}$ we need the following. In a dcpo
$X$, the way below relation $\ll$ is defined as: for $x,y \in X$,
$$\begin{array}{rcl}
x \ll y
& \Longleftrightarrow &
\mbox{for each directed }U\subseteq X, \mbox{ if }
      y\leq {\textstyle \bigvee U} \mbox{ then }
      \exin{z}{U}{x\leq z}.
\end{array}$$

\noindent A \emph{continuous poset} is then a dcpo in which for each
element $x\in X$ the set $\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x = \setin{y}{X}{y \ll x}$ is
directed and has $x$ as join. These elements way-below $x$ may be seen
as a (local) basis.

\auxproof{
It is easy to see that $x\ll y \implies x \leq y$. Thus $\ll$ is
anti-symmetric. It is obviously transitive. Further, if $x' \leq x \ll
y \leq y'$ then $x' \ll y'$. We shall make use below of the following
interpolation result, which is a mild generalization of~\cite[VII,
  Lemma 2.4]{Johnstone82}.

\begin{lem}
\label{InterpolationLem}
For each continuous function $f\colon X\rightarrow Y$ between
continuous posets $X,Y$ one has:
$$\begin{array}{rcl}
y \ll f(x)
& \Longrightarrow &
\exin{z}{X}{y \ll f(z) \mbox{ and } z\ll x}.
\end{array}$$
\end{lem}

\begin{myproof}
Given $x\in X$, consider the subset $W = \bigcup\set{\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(z)}{z
  \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \subseteq Y$ which is directed and has $f(x)$ as
supremum. Thus, if $y \ll f(x) = \bigvee W$, then $y \leq w$, for some
$w \in W$. But then $w \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(z)$ for some $z\in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}}
x$. Hence $y \ll f(z)$ and $z\ll x$. \qed

\auxproof{
We check that $W$ is directed: if $y_{1},y_{2}\in W$, say $y_{i}\ll
f(z_{i})$ for $z_{i}\ll x$, then, because $X$ is continuous, there is
a $z\ll x$ with $z_{i} \leq z$. Then $f(z_{i}) \leq f(z)$ and thus
$y_{i} \ll f(z)$. Since $Y$ is also continuous there is an $y\in Y$
with $y_{i} \leq y$ and $y\ll f(z)$. Hence $y\in W$.

Then:
$$\begin{array}{rcll}
\bigvee W
& = &
\bigvee \bigcup\set{\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(z)}{z \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \\
& = &
\bigvee \mathop{\downarrow}\!\set{\bigvee\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(z)}{z \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x}
   \qquad & \mbox{since $\bigvee$ is an algebra} \\
& = &
\bigvee \mathop{\downarrow}\!\set{f(z)}{z \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \\
& = &
\bigvee \set{f(z)}{z \in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \\
& = &
f(\bigvee\set{z}{z\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x})
   & \mbox{since $f$ is continuous} \\
& = &
f(x).
\end{array}$$
}

\end{myproof}
}

The following equivalence formed the basis for~\cite[Thm.~4.2]{Kock95}
(of which Theorem~\ref{KZCoAlgThm} is a special case).  The
equivalence of points~(1) and~(2) is known from the literature, see
e.g.~\cite[VII, Proposition~2.1]{Johnstone82},
\cite[Proposition~2.3]{Hoffmann79},
or~\cite[Theorem~I-1.10]{GierzHKLMS03}. The equivalence of points~(2)
and~(3) is given by Theorem~\ref{KZCoAlgThm}.

For a dcpo $X$, the following statements are equivalent.
\begin{enumerate}[(1)]
\item $X$ is a continuous poset;

\item The counit $\bigvee\colon\textsl{Idl}\xspace(X)\rightarrow X$ of the comonad
  $\overline{\textsl{Idl}\xspace}$ on \Cat{Dcpo}\xspace has a left adjoint (in \Cat{Dcpo}\xspace); it is
  $x\mapsto \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x$.

\item $X$ carries a (necessarily unique) $\overline{\textsl{Idl}\xspace}$-coalgebra
  structure $X \rightarrow \textsl{Idl}\xspace(X)$, which is also
  $\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}}(-)$.
\end{enumerate}

\auxproof{
We shall prove the equivalence of the first two points. In one
direction, if $X$ is a continuous dcpo, then $\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}}\colon X
\rightarrow \textsl{Idl}\xspace(X)$ is a continuous function: for a directed subset
$U\subseteq X$ one has:
$$\begin{array}{rcccccl}
y\in \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} U
& \Longleftrightarrow &
y \ll \bigvee U
& \smash{\stackrel{(*)}{\Longleftrightarrow}} &
\exin{x}{U}{y\ll x}
& \Longleftrightarrow &
y\in \bigcup\set{\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x}{x\in U}.
\end{array}$$

\noindent The implication $\smash{\stackrel{(*)}{\Longleftarrow}}$ is
obvious; for $\smash{\stackrel{(*)}{\Longrightarrow}}$, assume $y\ll
\bigvee U$; then by interpolation (Lemma~\ref{InterpolationLem}, with
$f = \idmap$), there is a $z$ with $y \ll z \ll \bigvee U$. But then
$z \leq x$ for some $x \in U$ and thus $y\ll x$. Next we have to
prove the adjoint correspondence:
$$\begin{prooftree}
\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x \;\subseteq\; U
\Justifies
x \;\leq\; \textstyle \bigvee U
\end{prooftree}$$

\noindent where $U\in\textsl{Idl}\xspace(X)$. For the downward direction, if
$\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x \subseteq U$, then $x = \bigvee\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x \leq \bigvee
U$. Upwards: if $x\leq\bigvee$ and $y\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x$, then $y\ll x$
and so $y\leq z$ for some $z\in U$. But then $y\in U$ since $U$ is a
downset.

Now assume the existence of a left adjoint $c\dashv \bigvee$ in \Cat{Dcpo}\xspace.
Hence $c$ is a continuous function $c\colon X\rightarrow \textsl{Idl}\xspace(X)$ with
$c(x)\subseteq U \Leftrightarrow x\leq \bigvee U$, for
$U\in\textsl{Idl}\xspace(X)$. We then have $\bigvee c(x) = x$, since in one
direction, $c(x)\subseteq c(x)$ yields $x\leq \bigvee c(x)$. And
conversely, from $x\leq \bigvee\mathop{\downarrow}\! x$ we get $c(x)\subseteq
\mathop{\downarrow}\! x$, and so $\bigvee c(x) \leq \bigvee\mathop{\downarrow}\! x = x$.

It thus suffices to prove $y\in c(x) \iff y\ll x$.
\begin{iteMize}{$\bullet$}
\item[($\Rightarrow$)] Let $y\in c(x)$. In order to show $y\ll x$,
  assume $x\leq \bigvee U$ for $U\subseteq X$ directed. Then $\mathop{\downarrow}\!
  U \in \textsl{Idl}\xspace(X)$ with $\bigvee U = \bigvee\mathop{\downarrow}\! U$. Since
  $x\leq\bigvee U = \bigvee\mathop{\downarrow}\! U$, the adjunction $c\dashv
  \bigvee$ yields $c(x) \subseteq \mathop{\downarrow}\! U$. Hence $y\in\mathop{\downarrow}\! U$,
  which gives a $z\in U$ with $y\leq z$.

\item[($\Leftarrow$)] If $y\ll x = \bigvee c(x)$, then $y\leq z$ for
some $z\in c(x)$. But then $y\in c(x)$, because the latter is
a downset. \qed
\end{iteMize}
}

\auxproof{
A map $f\colon X\rightarrow Y$ in $\Cat{Dcpo}\xspace$ is an
$\overline{T}$-coalgebra map if and only if for each $x\in X$,

$$\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(x)
=
\textsl{Idl}\xspace(f)(\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x)
=
\mathop{\downarrow}\!\set{f(y)}{y\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x}.$$

\noindent First assume $f$ is such a coalgebra map.  If $y\ll x$, then
$f(y)$, being in the set on the right, is also in the set on the
left. Thus $f(y) \ll f(x)$, and $f$ is monotone.

In the reverse direction, assume $f$ is monotone with respect to
$\ll$. We show that the above equation holds.
$$\!\!\!\begin{array}[b]{rcl}
y\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(x)
& \Longrightarrow &
y \ll f(x) \\[1mm]
& \Longrightarrow &
\ex{z}{y \ll f(z) \mbox{ and } z\ll x} \quad\mbox{by interpolation}
   \quad\quad \\[1mm]
& \Longrightarrow &
\ex{z}{y \leq f(z) \mbox{ and } z\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \\[1mm]
& \Longrightarrow &
y\in\mathop{\downarrow}\!\set{f(z)}{z\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x} \\[2mm]
y\in\mathop{\downarrow}\!\set{f(z)}{z\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x}
& \Longrightarrow &
\ex{z}{y \leq f(z) \mbox{ and } z\ll x} \\[1mm]
& \Longrightarrow &
\ex{z}{y \leq f(z) \mbox{ and } f(z)\ll f(x)}
     \quad\rlap{since $f$ is monotone}\\[1mm]
& \Longrightarrow &
y \ll f(x) \\[1mm]
& \Longrightarrow &
y\in\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} f(x).
\end{array}\eqno{\qEd}$$
}

\noindent Theorem~\ref{KZCoAlgBasisThm} says that another iteration
$\smash{\overline{\overline{\textsl{Idl}\xspace}}}$ yields nothing new.

\subsection{Frames over semi-lattices}\label{FrmMSLSubsec}

For a poset $X$, the set of its downsets:
$$\begin{array}{rcl}
\textsl{Dwn}\xspace(X)
& = &
\set{U\subseteq X}{U \mbox{ is downclosed}}
\end{array}$$

\noindent is a frame (or complete Heyting algebra, or locale),
see~\cite{Johnstone82}. If the poset $X$ has finite meets
$\top,\mathrel{\wedge}$, then the downset map $\mathop{\downarrow}\!\; \colon X\rightarrow
\textsl{Dwn}\xspace(X)$ preserves meets: $\mathop{\downarrow}\!\top = X$ and $\mathop{\downarrow}\!(x\mathrel{\wedge} y)
= \mathop{\downarrow}\! x \cap \mathop{\downarrow}\! y$. Hence it is a morphism in the category
\Cat{MSL}\xspace of meet semi-lattices. It is not hard to see that $\textsl{Dwn}\xspace$ is a
monad on \Cat{MSL}\xspace that is of Kock-Z{\"o}berlein type. For a (meet)
semi-lattice $X = (X, \top, \wedge)$ the following are equivalent.
\begin{enumerate}[(1)]
\item $X$ is a frame: $X$ has arbitrary joins and its finite meets
  distribute over these joins: $x \mathrel{\wedge} \big(\bigvee_{i}y_{i}\big) =
  \bigvee_{i}(x \mathrel{\wedge} y_{i})$;

\item The unit $\mathop{\downarrow}\!\; \colon  X \rightarrow  \textsl{Dwn}\xspace(X)$
  has a left adjoint in \Cat{MSL}\xspace---which is the join;

\item $X$ carries a (necessarily unique) algebra structure $\textsl{Dwn}\xspace(X)
  \rightarrow X$ in \Cat{MSL}\xspace, which is also the join.
\end{enumerate}

\noindent Moreover, the algebra maps are precisely the frame maps,
preserving arbitrary joins and finite meets; thus $\Cat{Frm}\xspace = \textsl{Alg}\xspace(\textsl{Dwn}\xspace)$.

\auxproof{
Despite Theorem~\ref{KZAlgThm}, we include an explicit (older, already
existing) proof.  For the implication $(1)\Rightarrow(2)$, assume $X$
is a frame. We show that the join $\bigvee$ forms a map $\textsl{Dwn}\xspace(X)
\rightarrow X$ in \Cat{MSL}\xspace. Clearly, $\bigvee\top = \bigvee X =
\top$. Preservation of meets follows because $X$ is a frame: for 2
downsets $U,V\in\textsl{Dwn}\xspace(X)$ we have,
$$\begin{array}{rcl}
(\bigvee U) \mathrel{\wedge} (\bigvee V)
& = &
\bigvee\set{(\bigvee U)\mathrel{\wedge} y}{y\in V} \\
& = &
\bigvee\set{\bigvee\set{x\mathrel{\wedge} y}{x\in U}}{y\in V} \\
& = &
\bigvee(U\cap V),
\end{array}$$

\noindent where the last equation holds because:

$(\leq)$ If $x\in U$ and $y\in V$, then $x\mathrel{\wedge} y \in U\cap V$
because $U,V$ are downsets, so $x\mathrel{\wedge} y \leq \bigvee(U\cap
V)$. Hence $\bigvee\set{x\mathrel{\wedge} y}{x\in U} \leq \bigvee(U\cap V)$,
and also $\bigvee\set{\bigvee\set{x\mathrel{\wedge} y}{x\in U}}{y\in V} \leq
\bigvee(U\cap V)$.

$(\geq)$ If $z\in U\cap V$, then $z\leq \bigvee\set{x\mathrel{\wedge} z}{x\in
  U}$, since $z\mathrel{\wedge} z = z$. Thus also $z \leq
\bigvee\set{\bigvee\set{x\mathrel{\wedge} y}{x\in U}}{y\in V}$. Hence
$\bigvee(U\cap V) \leq \bigvee\set{\bigvee\set{x\mathrel{\wedge} y}{x\in
    U}}{y\in V}$.

Next, the adjunction $\bigvee \dashv \mathop{\downarrow}\!$ involves the standard
correspondence:
$$\begin{prooftree}
\bigvee U \;\leq\; x
\Justifies
U \;\subseteq\; \mathop{\downarrow}\! x
\end{prooftree}$$

For the implication $(2)\Rightarrow(3)$ assume a left adjoint
$a\dashv\mathop{\downarrow}\!$. The adjoint correspondence immediately yields
that $a = \bigvee$, which in this case is a meet preserving map.
We need to show that it satisfies the algebra equations:
$$\begin{array}{rcl}
\big(\bigvee \mathrel{\circ} \mathop{\downarrow}\!\big)(x)
& = &
\bigvee\mathop{\downarrow}\! x \\
& = &
x \\
\big(\bigvee \mathrel{\circ} \textsl{Dwn}\xspace(\bigvee)\big)(A)
& = &
\bigvee\mathop{\downarrow}\!\set{\bigvee U}{U\in A} \\
& \smash{\stackrel{(*)}{=}} &
\bigvee\bigcup A \\
& = &
\big(\bigvee \mathrel{\circ} \bigcup\big)(A),
\end{array}$$

\noindent where the marked equation holds for the following
reasons.

$(\leq)$ Suppose $x\leq \bigvee U$ for $U\in A$. Then $U\subseteq
\bigcup A$ and thus $x \leq \bigvee U \leq \bigvee \bigcup A$.

$(\geq)$ Suppose $x\in\bigcup A$, say $x\in U\in A$. Then
$x \leq \bigvee U$, and thus $x\in \mathop{\downarrow}\!\set{\bigvee U}{U\in A}$.
Hence $x\leq \bigvee\mathop{\downarrow}\!\set{\bigvee U}{U\in A}$.

For the implication $(3)\Rightarrow(1)$ assume an algebra
$a\colon\textsl{Dwn}\xspace(X) \rightarrow X$. It satisfies $a(\mathop{\downarrow}\! x) = x$ and
$a(\mathop{\downarrow}\!\set{a(U)}{U\in A}) = a(\bigvee A)$ for $A\in\textsl{Dwn}\xspace^{2}(X)$.
We first prove that $a(U) = \bigvee U$.
\begin{iteMize}{$\bullet$}
\item $a(U)$ is an upperbound of $U$: if $x\in U$, then $\mathop{\downarrow}\! x
\subseteq U$ and thus $x = a(\mathop{\downarrow}\! x) \leq a(U)$.

\item $a(U)$ is the least upperbound: if $x\leq y$ for each $x\in U$,
then $U\subseteq\mathop{\downarrow}\! y$, and thus $a(U) \leq a(\mathop{\downarrow}\! y) = y$.
\end{iteMize}

We still have to show $a(U) \mathrel{\wedge} y = a(\set{x\mathrel{\wedge} y}{x\in U})$.
This follows because $a$ preserves meets:
$$\begin{array}{rcl}
a(U) \mathrel{\wedge} y
& = &
a(U) \mathrel{\wedge} a(\mathop{\downarrow}\! y) \\
& = &
a(U \cap \mathop{\downarrow}\! y) \\
& = &
a(\set{x\mathrel{\wedge} y}{x\in U}),
\end{array}$$

\noindent where the latter equation holds because:
$$\begin{array}{rcl}
U \cap \mathop{\downarrow}\! y
& = &
\set{x\mathrel{\wedge} y}{x\in U}
\end{array}$$

\noindent since:

$(\subseteq)$ If $x\in U \cap \mathop{\downarrow}\! y$, then $x\in U$ and
$x \leq y$. Hence $x \mathrel{\wedge} y = x\in U$.

$(\supseteq)$ If $x\in U$, then $x\mathrel{\wedge} y\in U$ and $x\mathrel{\wedge} y
\in \mathop{\downarrow}\! y$, so that $x\mathrel{\wedge} y \in U \cap \mathop{\downarrow}\! y$. \qed
}

In a next step, for a frame $X$, the following statements are
equivalent.
\begin{enumerate}[(1)]
\item $X$ is a stably continuous frame, \textit{i.e.}~a frame that is
  continuous as a dcpo, in which $\top\ll \top$, and also $x\ll y$ and
  $x\ll z$ implies $x\ll y\mathrel{\wedge} z$;

\item The counit $\bigvee\colon\textsl{Dwn}\xspace(X)\rightarrow X$ of the
comonad $\overline{\textsl{Dwn}\xspace}$ on \Cat{Frm}\xspace has a left adjoint in \Cat{Frm}\xspace;
it is $x\mapsto \mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} x$.

\item $X$ carries a (necessarily unique) $\overline{\textsl{Dwn}\xspace}$-coalgebra
  structure $X \rightarrow \textsl{Dwn}\xspace(X)$, which is also
  $\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}}(-)$. \qed
\end{enumerate}
One can show that coalgebra homomorphisms are the \textit{proper}
frame homomorphisms (from~\cite{BanaschewskiB88}) that preserve $\ll$.
We recall from~\cite[VII, 4.5]{Johnstone82} that for a sober
topological space $X$, its opens $\Omega(X)$ form a continuous lattice
iff X is a locally compact space.  Further, the stably continuous
frames are precisely the retracts of frames of the form $\textsl{Dwn}\xspace(X)$, for
$X$ a meet semi-lattice---here via the coreflection $\mathop{\rlap{$\downarrow$}\raisebox{.4ex}{$\downarrow$}} \dashv
\bigvee$.

\section{Examples in effectful programming}\label{ExceptionSec}

Since~\cite{Moggi91a} it is standard to describe the semantics of
(sequential) programs in the Kleisli category of a (strong) monad
$T$. The monad captures the computational effect involved, such as
partial computation via the lift monad, non-deterministic computation
via powerset $\powerset$, probabilistic computation via distribution
$\ensuremath{\mathcal{D}}$, exceptions via $E+(-)$, \textit{etc.} The combination of such
effects has also been studied, in terms of \emph{monad transformers},
see \textit{e.g.}~\cite{LiangHJ95,JaskelioffaM10}. Probably the most
well-known monad transformer is $T \mapsto T(E+-)$, which sends a
monad $T$ capturing some computational effect to the monad $T(E+-)$
which additionally incorporates exceptions (via a fixed exception
object $E$).

It has been observed before that this monad transformer $\ensuremath{\mathcal{E}}$, given by
$\ensuremath{\mathcal{E}}(T) = T(E+-)$, is a monad itself, on the category of monads. Hence
we can proceed as in Section~\ref{ComonadSec}, study its category
$\textsl{Alg}\xspace(\ensuremath{\mathcal{E}})$ of $\ensuremath{\mathcal{E}}$-algebras, with induced comonad $\overline{\ensuremath{\mathcal{E}}}
\colon \textsl{Alg}\xspace(\ensuremath{\mathcal{E}}) \rightarrow \textsl{Alg}\xspace(\ensuremath{\mathcal{E}})$, and with category of coalgebras
$\textsl{CoAlg}\xspace(\overline{\ensuremath{\mathcal{E}}})$. This has been done in~\cite{Levy06},
resulting in an intruiguing description of the `raise' and `handle'
operations associated with exceptions. Here we briefly recall these
main points, simply because the approach fits very well in the setting
of the current paper. We do not add any new material. The situation is
analogous to previous examples if one sees the algebra as the relevant
introduction rule and the coalgebra as the associated elimination rule
(for a new language construct).

Assume a distributive category $\cat{A}$, that is, a category with
finite products $(\times, 1)$ and coproducts $(+,0)$ such that
products distribute over coproducts, via (canonical) isomorphisms
$\smash{(X\times Y) + (X\times Z) \conglongrightarrow X\times (Y+Z)}$
and $\smash{0 \conglongrightarrow X\times 0}$.  We write
$\textsl{StMnd}\xspace(\cat{A})$ for the category of strong monads on $\cat{A}$, with
monad maps commuting with strength as morphisms. Strength $\ensuremath{\mathsf{st}}\colon
T(X) \times Y \rightarrow T(X\times Y)$ is standardly assumed in the
theory of monadic computation (see~\cite{Moggi91a}), where it is used
to handle computations in contexts.

\begin{thm}
\label{LevyThm}
In the setting described above,
\begin{enumerate}[\em(1)]
\item the mapping $\ensuremath{\mathcal{E}}(T) = T(E+-)$ is a monad on the category
  $\textsl{StMnd}\xspace(\cat{A})$ of strong monads on $\cat{A}$, giving rise to a
  situation:
$$\xymatrix@C-1pc{
& \textsl{Alg}\xspace(\ensuremath{\mathcal{E}})\ar@(ul,ur)^-{\overline{\ensuremath{\mathcal{E}}}=FU}\ar[dl]_{\dashv}\ar@/^3.5ex/[dr]
& \\
\textsl{StMnd}\xspace(\cat{A})\ar@(dl,dr)[]_-{\ensuremath{\mathcal{E}}}\ar@/^3.5ex/[ur]^{F}
   & & \textsl{CoAlg}\xspace\rlap{$(\overline{\ensuremath{\mathcal{E}}})$}\ar[ul]_{\dashv}
}$$

\item an $\ensuremath{\mathcal{E}}$-algebra corresponds to a ``throw'' map $E \rightarrow
  T(0)$;

\item a $\overline{\ensuremath{\mathcal{E}}}$-coalgebra corresponds to a `handle' (or
  `catch') family of maps $T(X) \rightarrow T(X+E)$, satisfying the
  equations for exception handling, see~\cite{Levy06}. \qed
\end{enumerate}
\end{thm}

The second point involves a bijective correspondence:
$$\hspace*{-5em}\begin{prooftree}
{\xymatrix{ \llap{$\ensuremath{\mathcal{E}}(T)=\;$}T(E+-)\ar@{=>}[r]^-{\sigma} & T
   \rlap{\quad\small map of monads, as $\ensuremath{\mathcal{E}}$-algebra}}}
\Justifies
{\xymatrix{ E\ar[r]_-{r} & T(0)}}
\end{prooftree}$$

\noindent This works as follows.
\begin{iteMize}{$\bullet$}
\item Given $\sigma$, take:
$$\xymatrix{
\widehat{\sigma} = \Big(E\ar[r]^-{\eta} &
   T(E)\ar[r]^-{T(\kappa_{1})}_-{\cong} & T(E+0)\ar[r]^-{\sigma_0} &
   T(0)\Big).
}$$

\item And given $r\colon E\rightarrow T(0)$, define
$\widehat{r}\colon T(E+-) \Rightarrow T$ with components:
$$\xymatrix{
\widehat{r}_{X} = \Big(T(E+X)\ar[rr]^-{T([T(!)\mathrel{\circ} r,\eta])} & &
   T^{2}(X)\ar[r]^-{\mu} & T(X)\Big).
}$$
\end{iteMize}

\noindent The coalgebra $T(X) \rightarrow T(X+E)$ in the third point
indeed does a catch, since after this coalgebra one can combine a
cotuple of a normal computation $f\colon X \rightarrow T(Y)$ with an
exception handler $g\colon E\rightarrow T(Y)$ in cotuple $[f,g] \colon
X+E \rightarrow T(Y)$, yielding a catch map $T(X) \rightarrow T(Y)$.

We refer to~\cite{Levy06} (and also~\cite{SchroderM04}) for more
information.

\auxproof{
We write $\eta,\mu$ of the monad of $T$, and define
$\eta^{\ensuremath{\mathcal{E}}(T)}$ and $\mu^{\ensuremath{\mathcal{E}}(T)}$ for $\ensuremath{\mathcal{E}}(T) = T(E+-)$,
in the following way.
$$\xymatrix@R-1.5pc{
\eta^{\ensuremath{\mathcal{E}}(T)} = \Big(X\ar[r]^-{\eta} & T(X)\ar[r]^-{T(\kappa_{2})} &
   T(E+X)\Big) \\
\mu^{\ensuremath{\mathcal{E}}(T)} = \Big(T(E + T(E + X))
   \ar[rr]^-{T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])}
   & & T^{2}(E+X)\ar[r]^-{\mu} & T(E+X)\Big)
}$$

\noindent Then:
$$\begin{array}{rcl}
\big(\mu^{\ensuremath{\mathcal{E}}(T)}_{X} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}(T)}_{T(E+X)}\big)
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ} T(\kappa_{2})
   \mathrel{\circ} \eta \\
& = &
\mu \mathrel{\circ} T(\idmap) \mathrel{\circ} \eta \\
& = &
\idmap \\
\big(\mu^{\ensuremath{\mathcal{E}}(T)}_{X} \mathrel{\circ} T(E+\eta^{\ensuremath{\mathcal{E}}(T)}_{X})\big)
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T([\kappa_{1}, \kappa_{2} \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \eta]) \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, T(\kappa_{2}) \mathrel{\circ} \eta]) \\
& = &
\mu \mathrel{\circ} T([\eta \mathrel{\circ} \kappa_{1}, \eta \mathrel{\circ} \kappa_{2}]) \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} T([\kappa_{1}, \kappa_{2}]) \\
& = &
\idmap \mathrel{\circ} T(\idmap) \\
& = &
\idmap \\
\big(\mu^{\ensuremath{\mathcal{E}}(T)}_{X} \mathrel{\circ} T(E+\mu^{\ensuremath{\mathcal{E}}(T)}_{X})\big)
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T([\kappa_{1}, \kappa_{2} \mathrel{\circ} \mu \mathrel{\circ}
      T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])]) \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \mu \mathrel{\circ}
      T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])]) \\
& = &
\mu \mathrel{\circ} T([\mu \mathrel{\circ} \eta \mathrel{\circ} T(\kappa_{1})\mathrel{\circ}\eta,
   \mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])]) \\
& = &
\mu \mathrel{\circ} T(\mu) \mathrel{\circ} T([T(T(\kappa_{1})\mathrel{\circ}\eta) \mathrel{\circ} \eta,
   T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])]) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   \mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \\
& = &
\big(\mu^{\ensuremath{\mathcal{E}}(T)}_{X} \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}(T)}_{T(E+X)}\big)
\end{array}$$

\noindent As strength map $\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}$ for $T(E+-)$ we take:
$$\xymatrix@C-1pc{
T(E+X)\times Y\ar[r]^-{\ensuremath{\mathsf{st}}} &
   T((E+X)\times Y)\ar[r]^-{T(\ensuremath{\mathsf{dis}})}_-{\cong} &
   T((E\times Y)+(X\times Y))\ar[rr]^-{T(\pi_{1}+\idmap)} & &
   T(E+(X\times Y)
}$$

\noindent This is a strength map indeed. We start with the
functor-properties of $\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}$.
$$\begin{array}{rcl}
\lefteqn{\ensuremath{\mathcal{E}}(T)(f\times g) \mathrel{\circ} \ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}} \\
& = &
T(\idmap+(f\times g)) \mathrel{\circ}
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+(f\times g)) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ}
   T((\idmap\times g)+(f\times g)) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ}
   T((\idmap+f)\times g) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ}
   (T(\idmap+f)\times g) \\
& = &
\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} (\ensuremath{\mathcal{E}}(T)(f)\times g) \\
\lefteqn{\ensuremath{\mathcal{E}}(T)(\pi_{1}) \mathrel{\circ} \ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}} \\
& = &
T(\idmap+\pi_{1}) \mathrel{\circ} T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+\pi_{1}) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\pi_{1} \\
\lefteqn{\ensuremath{\mathcal{E}}(T)(\alpha^{-1}) \mathrel{\circ} \ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ}
   (\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}\times\idmap)} \\
& = &
T(\idmap+\alpha^{-1}) \mathrel{\circ} T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}
   \mathrel{\circ}
   \big((T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}})\times\idmap\big) \\
& = &
T(\pi_{1}+\alpha^{-1}) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ}
   T((\pi_{1}+\idmap)\times\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}\times\idmap) \mathrel{\circ}
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\ensuremath{\mathsf{st}}\times\idmap) \\
& = &
T(\pi_{1}+\alpha^{-1}) \mathrel{\circ} T((\pi_{1}\times\idmap)+(\idmap\times\idmap))
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}\times\idmap) \mathrel{\circ}
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\ensuremath{\mathsf{st}}\times\idmap) \\
& = &
T((\pi_{1}\mathrel{\circ}\pi_{1})+\alpha^{-1})
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}\times\idmap) \mathrel{\circ}
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\ensuremath{\mathsf{st}}\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\alpha^{-1}+\alpha^{-1})
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}\times\idmap) \mathrel{\circ}
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\ensuremath{\mathsf{st}}\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\alpha^{-1}) \mathrel{\circ}
  \ensuremath{\mathsf{st}} \mathrel{\circ} (\ensuremath{\mathsf{st}}\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ} \alpha^{-1} \\
& = &
\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} \alpha^{-1}.
\end{array}$$

\noindent We turn to strenght, and $\eta,\mu$:
$$\begin{array}{rcl}
\lefteqn{\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} (\eta^{\ensuremath{\mathcal{E}}(T)}\times\idmap)} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ}
   \big((T(\kappa_{2})\mathrel{\circ} \eta)\times\idmap\big) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\kappa_{2}\times\idmap) \mathrel{\circ}
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\eta\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
\eta^{\ensuremath{\mathcal{E}}(T)} \\
\lefteqn{\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} (\mu^{\ensuremath{\mathcal{E}}(T)}\times\idmap)} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ}
   ((\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]))\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \mu \mathrel{\circ}  T(\ensuremath{\mathsf{st}}) \mathrel{\circ} \ensuremath{\mathsf{st}}
   \mathrel{\circ} (T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap])\times\idmap) \\
& = &
\mu \mathrel{\circ} T^{2}(\pi_{1}+\idmap) \mathrel{\circ} T^{2}(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{st}})
   \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T^{2}(\pi_{1}+\idmap) \mathrel{\circ} T^{2}(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{st}})
   \mathrel{\circ} T(\nabla\times\idmap) \mathrel{\circ}
   T((T(\kappa_{1})\mathrel{\circ}\eta) + \idmap)\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T^{2}(\pi_{1}+\idmap) \mathrel{\circ} T^{2}(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{st}})
   \mathrel{\circ} T(\nabla) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ}
   T((T(\kappa_{1})\mathrel{\circ}\eta) + \idmap)\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T^{2}(\pi_{1}+\idmap) \mathrel{\circ} T^{2}(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{st}})
   \mathrel{\circ} T(\nabla) \mathrel{\circ}
   T(((T(\kappa_{1})\mathrel{\circ}\eta)\times\idmap) + (\idmap\times\idmap))
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T^{2}(\pi_{1}+\idmap) \mathrel{\circ} T^{2}(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\ensuremath{\mathsf{st}})
   \mathrel{\circ} T([(T(\kappa_{1})\mathrel{\circ}\eta)\times\idmap, \idmap])
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}
   \mathrel{\circ} (T(\kappa_{1})\times\idmap) \mathrel{\circ} (\eta\times\idmap),
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}])
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\pi_{1}+\idmap) \mathrel{\circ}
   T(\ensuremath{\mathsf{dis}} \mathrel{\circ} (\kappa_{1}\times\idmap)) \mathrel{\circ} \ensuremath{\mathsf{st}}
   \mathrel{\circ} (\eta\times\idmap),
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}])
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\pi_{1}+\idmap) \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta,
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}])
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1} \mathrel{\circ} \pi_{1}) \mathrel{\circ} \eta,
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}])
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta \mathrel{\circ} \pi_{1},
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}}]) \mathrel{\circ}
   T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T(\pi_{1}+(T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}})) \mathrel{\circ}
   T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T(\idmap+(T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}})) \mathrel{\circ}
   T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} T(E+\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}) \mathrel{\circ}
\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}.
\end{array}$$

Next we show that $\ensuremath{\mathcal{E}}$, given by $\ensuremath{\mathcal{E}}(T) = T(E+-)$
is a monad on $\textsl{StMnd}\xspace(\cat{A})$. For a map of strong monads
$\sigma\colon T\Rightarrow S$ one has $\ensuremath{\mathcal{E}}(\sigma) \colon
\ensuremath{\mathcal{E}}(T) \rightarrow \ensuremath{\mathcal{E}}(S)$ with components:
$$\begin{array}{rcl}
\ensuremath{\mathcal{E}}(\sigma)_{X}
& = &
\sigma_{E+X} \colon T(E+X) \longrightarrow S(E+X).
\end{array}$$

\noindent This $\ensuremath{\mathcal{E}}(\sigma)$ is a map of monads:
$$\begin{array}{rcl}
\ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}(T)}
& = &
\sigma \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
S(\kappa_{2}) \mathrel{\circ} \sigma \mathrel{\circ} \eta \\
& = &
S(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
\eta^{\ensuremath{\mathcal{E}}(S)} \\
\ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}(T)}
& = &
\sigma \mathrel{\circ} \mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \\
& = &
\mu \mathrel{\circ} \sigma \mathrel{\circ} T(\sigma) \mathrel{\circ}
   T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \\
& = &
\mu \mathrel{\circ} \sigma \mathrel{\circ}
   T([\sigma \mathrel{\circ} T(\kappa_{1})\mathrel{\circ}\eta, \sigma]) \\
& = &
\mu \mathrel{\circ} S([S(\kappa_{1})\mathrel{\circ} \sigma \mathrel{\circ}\eta, \sigma])
   \mathrel{\circ} \sigma \\
& = &
\mu \mathrel{\circ} S([S(\kappa_{1})\mathrel{\circ} \eta, \sigma])
   \mathrel{\circ} \sigma \\
& = &
\mu \mathrel{\circ} S([S(\kappa_{1})\mathrel{\circ}\eta, \idmap])
   \mathrel{\circ} S(\idmap+\sigma) \mathrel{\circ} \sigma \\
& = &
\mu \mathrel{\circ} S([S(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ} \sigma
   \mathrel{\circ} T(\idmap+\sigma) \\
& = &
\mu^{\ensuremath{\mathcal{E}}(S)} \mathrel{\circ} \ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ}
   \ensuremath{\mathcal{E}}(T)(\ensuremath{\mathcal{E}}(\sigma)) \\
\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} (\ensuremath{\mathcal{E}}(\sigma)\times\idmap)
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ} (\sigma\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \sigma \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\sigma \mathrel{\circ} S(\pi_{1}+\idmap) \mathrel{\circ} S(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ} \ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(S)}.
\end{array}$$

The unit $\eta^{\ensuremath{\mathcal{E}}}_{T} \colon
T \Rightarrow \ensuremath{\mathcal{E}}(T)$ has components:
$$\begin{array}{rcl}
\eta^{\ensuremath{\mathcal{E}}}_{T,X}
& = &
T(\kappa_{2}) \colon T(X) \longrightarrow T(E+X).
\end{array}$$

\noindent Naturality means that for a map of strong monads
$\sigma\colon T\Rightarrow S$ one has:
$$\begin{array}{rcl}
\ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}}_{T}
& = &
\sigma \mathrel{\circ} T(\kappa_{2}) \\
& = &
S(\kappa_{2}) \mathrel{\circ} \sigma \\
& = &
\eta^{\ensuremath{\mathcal{E}}}_{S} \mathrel{\circ} \sigma.
\end{array}$$

\noindent Next, we check that $\eta^{\ensuremath{\mathcal{E}}}$ is a map of strong
monads:
$$\begin{array}{rcl}
\eta^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \eta
& = &
T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
\eta^{\ensuremath{\mathcal{E}}(T)} \\
\mu^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}} \mathrel{\circ} T(\eta^{\ensuremath{\mathcal{E}}})
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ} T(\kappa_{2})
   \mathrel{\circ} T^{2}(\kappa_{2}) \\
& = &
\mu \mathrel{\circ} T^{2}(\kappa_{2}) \\
& = &
T(\kappa_{2}) \mathrel{\circ} \mu \\
& = &
\eta^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \mu \\
\ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} (\eta^{\ensuremath{\mathcal{E}}}\times\idmap)
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ}
   (T(\kappa_{2})\times\idmap) \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} T(\kappa_{2}\times\idmap)
  \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\pi_{1}+\idmap) \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
T(\kappa_{2}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\eta^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \ensuremath{\mathsf{st}}
\end{array}$$

\noindent Similarly there is a multiplication $\mu^{\ensuremath{\mathcal{E}}}_{T}
\colon \ensuremath{\mathcal{E}}^{2}(T) \Rightarrow \ensuremath{\mathcal{E}}(T)$, with
components:
$$\begin{array}{rcl}
\mu^{\ensuremath{\mathcal{E}}}_{T,X}
& = &
T([\kappa_{1},\idmap])\colon T(E + (E+X)) \longrightarrow T(E+X)
\end{array}$$

\noindent This $\mu^{\ensuremath{\mathcal{E}}}$ is natural:
$$\begin{array}{rcl}
\mu^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \ensuremath{\mathcal{E}}^{2}(\sigma)
& = &
T([\kappa_{1},\idmap]) \mathrel{\circ} \sigma \\
& = &
\sigma \mathrel{\circ} S([\kappa_{1},\idmap]) \\
& = &
\ensuremath{\mathcal{E}}(\sigma) \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}}.
\end{array}$$

\noindent Moreover, $\mu^{\ensuremath{\mathcal{E}}}$ is a map of strong monads:
$$\begin{array}{rcl}
\mu^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}^{2}(T)}
& = &
T([\kappa_{1},\idmap]) \mathrel{\circ} \ensuremath{\mathcal{E}}(T)(\kappa_{2}) \mathrel{\circ}
   \eta^{\ensuremath{\mathcal{E}}(T)} \\
& = &
T([\kappa_{1},\idmap]) \mathrel{\circ} T(\idmap+\kappa_{2}) \mathrel{\circ}
   T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
T([\kappa_{1},\kappa_{2}]) \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
\eta^{\ensuremath{\mathcal{E}}(T)}.
\end{array}$$

\noindent For the multiplication law we need to clarify our
notation. We have:
$$\xymatrix@R-1.5pc@C+1pc{
T(E+T(E+-)) = \ensuremath{\mathcal{E}}(T)^{2}\ar@{=>}[r]^-{\mu^{\ensuremath{\mathcal{E}}(T)}} &
   \ensuremath{\mathcal{E}}(T) \\
T(E+(E+-)) = \ensuremath{\mathcal{E}}^{2}(T)\ar@{=>}[r]^-{\mu^{\ensuremath{\mathcal{E}}}_{T}} &
   \ensuremath{\mathcal{E}}(T) \\
}$$

\noindent The following diagram thus needs to commute.
$$\xymatrix@C+1pc{
\ensuremath{\mathcal{E}}^{2}(T)\ensuremath{\mathcal{E}}^{2}(T)\ar[d]_{\mu^{\ensuremath{\mathcal{E}}^{2}(T)}}
      \ar[r]^-{\mu^{\ensuremath{\mathcal{E}}}_{\ensuremath{\mathcal{E}}^{2}(T)}} &
   \ensuremath{\mathcal{E}}(T)\ensuremath{\mathcal{E}}^{2}(T)
      \ar[r]^-{\ensuremath{\mathcal{E}}(T)\mu^{\ensuremath{\mathcal{E}}}_{T}} &
   \ensuremath{\mathcal{E}}(T)\ensuremath{\mathcal{E}}(T)\ar[d]^{\mu^{\ensuremath{\mathcal{E}}(T)}} \\
\ensuremath{\mathcal{E}}^{2}(T)\ar[rr]_-{\mu^{\ensuremath{\mathcal{E}}}_{T}} & & \ensuremath{\mathcal{E}}(T)
}$$

\noindent The vertical multiplication $\mu^{\ensuremath{\mathcal{E}}^{2}(T)}$ on
the left is the following composite.
$$\xymatrix@R-1.5pc{
\ensuremath{\mathcal{E}}^{2}(T)\ensuremath{\mathcal{E}}^{2}(T)(X)\ar@{=}[d]
   \ar[rr]^-{\ensuremath{\mathcal{E}}(T)([\ensuremath{\mathcal{E}}(T)(\kappa_{1}) \mathrel{\circ}
       \eta^{\ensuremath{\mathcal{E}}(T)}_{E},\idmap])} & &
   \ensuremath{\mathcal{E}}(T)^{2}(E+X)\ar@{=}[d]\ar[r]^-{\mu^{\ensuremath{\mathcal{E}}(T)}_{E+X}} &
   \ensuremath{\mathcal{E}}^{2}(T)(X)\ar@{=}[d] \\
T(E+(E+T(E+(E+X))))\ar@/_4ex/[rr]_-{T(\idmap+([T(\idmap+\kappa_{1})
   \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta_{E}, \idmap]))} & &
   T(E+T(E+(E+X)))\ar@/_4ex/[dr]_-{\mu \mathrel{\circ}
       T([T(\kappa_{1})\mathrel{\circ}\eta,\idmap])}  &
   T(E+(E+X))\ar@{=}[d] \\
& & & \ensuremath{\mathcal{E}}(T)(E+X)
}$$

$$\begin{array}{rcl}
\lefteqn{\mu^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} \ensuremath{\mathcal{E}}(T)\mu^{\ensuremath{\mathcal{E}}}_{T}
   \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}}_{\ensuremath{\mathcal{E}}^{2}(T)}} \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, \idmap]) \mathrel{\circ}
   T(\idmap+T([\kappa_{1},\idmap])) \mathrel{\circ} T([\kappa_{1},\idmap]) \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta, T([\kappa_{1},\idmap])])
   \mathrel{\circ} T([\kappa_{1},\idmap]) \\
& = &
\mu \mathrel{\circ} T([T(\kappa_{1})\mathrel{\circ}\eta,
   [T(\kappa_{1}) \mathrel{\circ} \eta, T([\kappa_{1},\idmap])]]) \\
& = &
\mu \mathrel{\circ} T^{2}([\kappa_{1},\idmap]) \mathrel{\circ}
   T([T(\kappa_{1})\mathrel{\circ}\eta, [T(\kappa_{1}) \mathrel{\circ} \eta, \idmap]]) \\
& = &
\mu \mathrel{\circ} T^{2}([\kappa_{1},\idmap]) \mathrel{\circ}
   T([T(\kappa_{1})\mathrel{\circ}\eta,\idmap]) \mathrel{\circ}
   T(\idmap+([T(\kappa_{1}) \mathrel{\circ} \eta, \idmap])) \\
& = &
T([\kappa_{1},\idmap]) \mathrel{\circ} \mu \mathrel{\circ}
   T([T(\kappa_{1})\mathrel{\circ}\eta,\idmap]) \mathrel{\circ}
   T(\idmap+([T(\idmap+\kappa_{1}) \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ}
   \eta, \idmap])) \\
& = &
\mu^{\ensuremath{\mathcal{E}}} \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}^{2}(T)}
\end{array}$$

Next we prove that there is a correspondence between
$\ensuremath{\mathcal{E}}$-algebras with carrier $T\in\textsl{StMnd}\xspace(\cat{A})$ and certain
maps $E\rightarrow T(0)$ in $\cat{A}$:
$$\begin{prooftree}
{\xymatrix{ \llap{$T(E+-)=\;$}\ensuremath{\mathcal{E}}(T)\ar@{=>}[r]^-{\sigma} & T
   \rlap{\quad algebra}}}
\Justifies
{\xymatrix{ E \ar[r]_-{r} & T(0) }}
\end{prooftree}$$

\noindent This works as follows (see~\cite{Levy06}).
\begin{iteMize}{$\bullet$}
\item Given $\sigma$, take:
$$\xymatrix{
\overline{\sigma} = \Big(E\ar[r]^{\eta} &
   T(E)\ar[r]^-{T(\kappa_{1})}_-{\cong} & T(E+0)\ar[r]^-{\sigma_0} &
   T(0)\Big).
}$$

\item Conversely, given $r\colon E\rightarrow T(0)$, define
$\overline{r}\colon T(E+-) \Rightarrow T$ with components:
$$\xymatrix{
\overline{r}_{X} = \Big(T(E+X)\ar[rr]^-{T([T(!)\mathrel{\circ} r,\eta])} & &
   T^{2}(X)\ar[r]^-{\mu} & T(X)\Big).
}$$

\noindent We start with naturality: for $f\colon X\rightarrow Y$,
$$\begin{array}{rcl}
\overline{r}_{Y} \mathrel{\circ} \ensuremath{\mathcal{E}}(T)(f)
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} T(\idmap+f) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta \mathrel{\circ} f]) \\
& = &
\mu \mathrel{\circ} T([T(f) \mathrel{\circ} T(!)\mathrel{\circ} r, T(f) \mathrel{\circ} \eta]) \\
& = &
\mu \mathrel{\circ} T^{2}(f) \mathrel{\circ} T([T(!)\mathrel{\circ} r, \eta]) \\
& = &
T(f) \mathrel{\circ} \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r, \eta]) \\
& = &
T(f) \mathrel{\circ} \overline{r}_{X}
\end{array}$$

\noindent Further, $\overline{r}$ is a map of monads:
$$\begin{array}{rcl}
\overline{r} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}(T)}
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} \eta \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} \eta \\
& = &
\eta \\
\overline{r} \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}(T)}
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} \mu \mathrel{\circ}
   T([T(\kappa_{1}) \mathrel{\circ} \eta, \idmap]) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ}
   T([T(\kappa_{1}) \mathrel{\circ} \eta, \idmap]) \\
& = &
\mu \mathrel{\circ} T(\mu) \mathrel{\circ}
   T([T(T(!)\mathrel{\circ} r) \mathrel{\circ} \eta, T([T(!)\mathrel{\circ} r,\eta])]) \\
& = &
\mu \mathrel{\circ} T([\mu \mathrel{\circ} T^{2}(!)\mathrel{\circ} T(r) \mathrel{\circ} \eta,
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta])]) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} \mu \mathrel{\circ} \eta \mathrel{\circ} r,
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta])]) \\
& = &
\mu \mathrel{\circ} T([\mu \mathrel{\circ} T(\eta \mathrel{\circ}\, !)\mathrel{\circ} r,
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta])]) \\
& = &
\mu \mathrel{\circ} T(\mu) \mathrel{\circ}
   T([T(!)\mathrel{\circ} r, T([T(!)\mathrel{\circ} r,\eta])]) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ}
   T([T(!)\mathrel{\circ} r, \idmap]) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} \mu \mathrel{\circ}
   T([T(!)\mathrel{\circ} r, \idmap]) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} \mu \mathrel{\circ}
   T(\mu) \mathrel{\circ} T([T(\eta \mathrel{\circ} !)\mathrel{\circ} r,\eta]) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} \mu \mathrel{\circ}
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ}
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \\
& = &
\mu \mathrel{\circ} T(\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta])) \mathrel{\circ}
   \mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \\
& = &
\mu \mathrel{\circ} T(\overline{r}) \mathrel{\circ} \overline{r} \\
\ensuremath{\mathsf{st}} \mathrel{\circ} (\overline{r}\times\idmap)
& = &
\ensuremath{\mathsf{st}} \mathrel{\circ} ((\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]))\times\idmap) \\
& = &
\mu \mathrel{\circ} T(\ensuremath{\mathsf{st}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \mathrel{\circ} (T([T(!)\mathrel{\circ} r,\eta])\times\idmap) \\
& = &
\mu \mathrel{\circ} T(\ensuremath{\mathsf{st}}) \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T(\ensuremath{\mathsf{st}}) \mathrel{\circ} T(\nabla\times\idmap) \mathrel{\circ}
    T(((T(!)\mathrel{\circ} r) + \eta)\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T(\ensuremath{\mathsf{st}}) \mathrel{\circ} T(\nabla) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ}
    T(((T(!)\mathrel{\circ} r) + \eta)\times\idmap) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T(\ensuremath{\mathsf{st}}) \mathrel{\circ} T(\nabla) \mathrel{\circ}
    T(((T(!)\mathrel{\circ} r)\times\idmap) + (\eta\times\idmap))
   \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([\ensuremath{\mathsf{st}} \mathrel{\circ} (T(!)\times\idmap) \mathrel{\circ} (r\times\idmap),
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\eta\times\idmap)]) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& \smash{\stackrel{(*)}{=}} &
\mu \mathrel{\circ} T([T(!) \mathrel{\circ} \pi_{1} \mathrel{\circ} (r\times\idmap),
   \ensuremath{\mathsf{st}} \mathrel{\circ} (\eta\times\idmap)]) \mathrel{\circ} T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r \mathrel{\circ} \pi_{1},\eta]) \mathrel{\circ}
   T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} r,\eta]) \mathrel{\circ} T(\pi_{1}+\idmap) \mathrel{\circ}
   T(\ensuremath{\mathsf{dis}}) \mathrel{\circ} \ensuremath{\mathsf{st}} \\
& = &
\overline{r} \mathrel{\circ} \ensuremath{\mathsf{st}}^{\ensuremath{\mathcal{E}}(T)}.
\end{array}$$

\noindent The marked equation $(*)$ holds because $\ensuremath{\mathsf{st}} \mathrel{\circ}
(T(!)\times\idmap) = T(!) \mathrel{\circ} \pi_{1}$. This follows from the
following diagram which commutes, since $0\times Y \cong 0$ by
distributivity.
$$\xymatrix{
& T(0)\times Y\ar[d]_{\idmap\times\,!}\ar@/_4ex/[ddl]_{\pi_1}\ar[dr]^{\ensuremath{\mathsf{st}}}
      \ar[rrr]^-{T(!)\times\idmap} & & & T(X)\times Y\ar[d]^{\ensuremath{\mathsf{st}}} \\
& T(0)\times 1\ar[dl]_{\pi_1}\ar[dr]^{\ensuremath{\mathsf{st}}} &
   T(0\times Y)\ar[d]^{\cong}\ar[rr]^-{T(!\times\idmap)} & &
   T(X\times Y) \\
T(0)\ar@/_12ex/[rrrru]^-{T(!)} & &
   T(0\times 1)\ar[ll]_-{T(\pi_{1})}^-{\cong}
}$$

Finally, we also have to check that $\overline{r}$ satisfies
the equations for an $\ensuremath{\mathcal{E}}$-algebra:
$$\begin{array}{rcl}
\overline{r} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}}
& = &
\mu \mathrel{\circ} T([T(!) \mathrel{\circ} r, \eta]) \mathrel{\circ} T(\kappa_{2}) \\
& = &
\mu \mathrel{\circ} T(\eta) \\
& = &
\idmap \\
\overline{r} \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}}
& = &
\mu \mathrel{\circ} T([T(!) \mathrel{\circ} r, \eta]) \mathrel{\circ} T([\kappa_{1},\idmap]) \\
& = &
\mu \mathrel{\circ} T([T(!) \mathrel{\circ} r, [T(!) \mathrel{\circ} r, \eta]]) \\
& = &
\mu \mathrel{\circ} T([\mu \mathrel{\circ} T(\eta\mathrel{\circ}\,!) \mathrel{\circ} r,
   \mu \mathrel{\circ} \eta \mathrel{\circ} [T(!) \mathrel{\circ} r, \eta]]) \\
& = &
\mu \mathrel{\circ} T(\mu) \mathrel{\circ}
   T([T(!) \mathrel{\circ} r, T([T(!) \mathrel{\circ} r, \eta]) \mathrel{\circ} \eta]) \\
& = &
\mu \mathrel{\circ} \mu \mathrel{\circ} T^{2}([T(!) \mathrel{\circ} r, \eta]) \mathrel{\circ}
   T([T(!) \mathrel{\circ} r, \eta]) \\
& = &
\mu \mathrel{\circ} T([T(!) \mathrel{\circ} r, \eta]) \mathrel{\circ} \mu \mathrel{\circ}
   T([T(!) \mathrel{\circ} r, \eta]) \\
& = &
\overline{r} \mathrel{\circ} \ensuremath{\mathcal{E}}(\overline{r}).
\end{array}$$

\end{iteMize}

\noindent We do have a bijective correspondence, since:
$$\begin{array}{rcl}
\overline{\overline{\sigma}}_{X}
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} \overline{\sigma}, \eta]) \\
& = &
\mu \mathrel{\circ} T([T(!)\mathrel{\circ} \sigma_{0} \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta,
   \eta]) \\
& = &
\mu \mathrel{\circ} T([\sigma_{X} \mathrel{\circ} T(\idmap+\,!) \mathrel{\circ} T(\kappa_{1})
    \mathrel{\circ} \eta, \eta]) \\
& = &
\mu \mathrel{\circ} T([\sigma_{X} \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta, \eta]) \\
& = &
\mu \mathrel{\circ} T([\sigma_{X} \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta,
   \sigma_{X} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}(T)}]) \\
& = &
\mu \mathrel{\circ} T(\sigma_{X}) \mathrel{\circ} T([T(\kappa_{1}) \mathrel{\circ} \eta,
   T(\kappa_{2}) \mathrel{\circ} \eta]) \\
& = &
\mu \mathrel{\circ} T(\sigma_{X}) \mathrel{\circ} T([\eta \mathrel{\circ} \kappa_{1},
   \eta \mathrel{\circ} \kappa_{2}]) \\
& = &
\mu \mathrel{\circ} T(\sigma_{X}) \mathrel{\circ} T(\eta) \\
& = &
\mu \mathrel{\circ} T(\sigma_{X}) \mathrel{\circ} \sigma_{X} \mathrel{\circ} \eta^{\ensuremath{\mathcal{E}}}
   \mathrel{\circ} T(\eta) \\
& = &
\sigma_{X} \mathrel{\circ} \mu^{\ensuremath{\mathcal{E}}(T)} \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ}
   T(\eta) \\
& = &
\sigma_{X} \mathrel{\circ} \mu \mathrel{\circ} T([T(\kappa_{1}) \mathrel{\circ} \eta, \idmap])
   \mathrel{\circ} T(\kappa_{2}) \mathrel{\circ} T(\eta) \\
& = &
\sigma_{X} \mathrel{\circ} \mu \mathrel{\circ} T(\eta) \\
& = &
\sigma_{X} \\
\overline{\overline{r}}
& = &
\overline{r}_{0} \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta \\
& = &
\mu_{0} \mathrel{\circ} T([r, \eta_{0}]) \mathrel{\circ} T(\kappa_{1}) \mathrel{\circ} \eta \\
& = &
\mu_{0} \mathrel{\circ} T(r) \mathrel{\circ} \eta \\
& = &
\mu_{0} \mathrel{\circ} \eta \mathrel{\circ} r  \\
& = &
r.
\end{array}$$
}

\section{Comonoids from bases}\label{ComonoidSec}

A recent insight, see~\cite{CoeckePV12}, is that orthonormal bases in
finite-dimensional Hilbert spaces can be described via so-called
Frobenius algebras. Orthonormal bases are very important in quantum
theory because they provide a `perspective' for a measurement on a
system. The algebraic re-description of bases in terms of Frobenius
algebras is influential because it gives rise to a diagrammatic
calculus for quantum protocols, see \textit{e.g.}~\cite{Coecke10a}.
In the present section we show how the coalgebra-as-basis perspective
gives rise to comonoidal structure for copy and delete --- and thus to
the essential part of a Frobenius algebra structure.

In general, such a Frobenius algebra consists of an object carrying
both a monoid and a comonoid structure that interact appropriately. In
the self-dual category of Hilbert spaces, it suffices to have either a
monoid or a comonoid, since the dual is induced by the dagger /
adjoint transpose $(-)^{\dag}$. In this section we show that the kind
of coalgebras (on algebras) considered in this paper also give rise to
comonoids, assuming that the category of algebras has monoidal
(tensor) structure.

In a (symmetric) monoidal category $\cat{A}$ a comonoid is the dual of
a monoid, given by maps $\smash{I \stackrel{u}{\leftarrow} X
  \stackrel{d}{\rightarrow} X\otimes X}$ satisfying the duals of the
monoid equations. Such comonoids are used for copying and deletion, in
linear and quantum logic. If $\otimes$ is cartesian product $\times$,
each object carries a unique comonoid structure
$\smash{1\stackrel{!}{\leftarrow} X \stackrel{\Delta}{\rightarrow}
  X\times X}$. The no-cloning theorem in quantum mechanics (due to
Dieks, Wootters and Zurek) says that copying arbitrary states is
impossible. But copying wrt.\ a basis is allowed,
see~\cite{NielsenC00,CoeckePV12,Abramsky10b}.

If a monad $T$ on a symmetric monoidal category $\cat{A}$ is a
commutative (aka.\ symmetric monoidal) monad, and the category
$\textsl{Alg}\xspace(T)$ has enough coequalisers, then it is also symmetric monoidal,
and the free functor $F\colon\cat{A}\rightarrow\textsl{Alg}\xspace(T)$ preserves this
monoidal structure (via the isomorphism $\xi$ used below). This
classical result goes back to~\cite{Kock71a,Kock71b}. We shall use it
for the special case where the monoidal structure on the base category
$\cat{A}$ is cartesian.

\begin{prop}
\label{ComonoidProp}
In the setting described above, assume the category of algebras
$\textsl{Alg}\xspace(T)$ is symmetric monoidal, for a commutative monad $T$ on a
cartesian category $\cat{A}$. Each $\overline{T}$-coalgebra / basis
$b\colon X\rightarrow T(X)$, say on algebra $a\colon T(X)\rightarrow
X$, gives rise to a commutative comonoid in $\textsl{Alg}\xspace(T)$ by:
\begin{equation}
\label{ComonoidDefEqn}
\begin{array}{rcl}
d_{b}
& = &
{\xymatrix@C-.5pc{
\Big(X\ar[r]^-{b} & TX\ar[r]^-{T(\Delta)} &
   T(X\times X)\ar[r]^-{\xi^{-1}}_-{\cong} &
   T(X)\otimes T(X)\ar[r]^-{a\otimes a} & X\otimes X\Big)
}} \\[-.3em]
u_{b}
& = &
{\xymatrix@C-.5pc{
\Big(X\ar[r]^-{b} & T(X)\ar[r]^-{T(!)} & T(1)=I\Big),
}}
\end{array}
\end{equation}

\noindent where we use the underlying comonoid structure
$\smash{1\stackrel{!}{\leftarrow} X \stackrel{\Delta}{\rightarrow}
  X\times X}$ on $X$ in the underlying category $\cat{A}$.
\end{prop}

\begin{myproof}
It is not hard to see that these $d_b$ and $u_b$ are maps of algebras:
$$\mu_{1} \mathrel{\circ} T(u_{b})
=
\mu_{1} \mathrel{\circ} T^{2}(!) \mathrel{\circ} T(b)
=
T(!) \mathrel{\circ} \mu_{X} \mathrel{\circ} T(b)
=
T(!) \mathrel{\circ} b \mathrel{\circ} a
=
u_{b} \mathrel{\circ} a.$$

\noindent The verification of the comonoid properties involves lengthy
calculations, which are basically straightforward. We just show that
$u$ is neutral element for $d$, using the equations from
Definition~\ref{BasisDef}.
$$\begin{array}[b]{rcl}
(u_{b}\otimes\idmap) \mathrel{\circ} d_{d}
& = &
(T(!)\otimes\idmap) \mathrel{\circ} (b\otimes\idmap) \mathrel{\circ} (a \otimes a)
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes\idmap) \mathrel{\circ} (\mu\otimes\idmap) \mathrel{\circ} (T(b)\otimes a)
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes T(a)) \mathrel{\circ} (T(b)\otimes T(b))
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(b\times b) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(\eta\times \eta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} (T(\eta)\otimes T(\eta)) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} (T(!)\otimes \idmap) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(!\times \idmap)
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\lambda^{-1}) \mathrel{\circ} b
   \qquad \mbox{where }\lambda\colon 1\times X \conglongrightarrow X \\
& = &
(\idmap\otimes a) \mathrel{\circ} \lambda^{-1} \mathrel{\circ} b
   \qquad \mbox{since $\xi$ is monoidal, where $\lambda \colon
   I \otimes X  \conglongrightarrow X$} \\
& = &
\lambda^{-1} \mathrel{\circ} a \mathrel{\circ} b \\
& = &
\lambda^{-1} \colon X\conglongrightarrow I\otimes X.
\end{array}\eqno{\qEd}$$

\end{myproof}

\auxproof{
We first check that $u_{b}, d_{b}$ are maps of algebras:
$$\begin{array}{rcl}
\mu \mathrel{\circ} T(u_{b})
& = &
\mu \mathrel{\circ} T^{2}(!) \mathrel{\circ} T(b) \\
& = &
T(!) \mathrel{\circ} \mu \mathrel{\circ} T(b) \\
& = &
T(!) \mathrel{\circ} b \mathrel{\circ} a \\
& = &
u_{b} \mathrel{\circ} a \\
d_{b} \mathrel{\circ} a
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \mathrel{\circ} a \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} \mu \mathrel{\circ} T(b) \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} \mu \mathrel{\circ} T^{2}(\Delta) \mathrel{\circ} T(b) \\
& = &
(a\otimes a) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\xi^{-1})
   \mathrel{\circ} T(T(\Delta) \mathrel{\circ} b) \\
& = &
(a\otimes a) \mathrel{\circ} (T(a)\otimes T(a)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b) \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(a\otimes a) \mathrel{\circ} T(\xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b) \\
& = &
(a\boxtimes a) \mathrel{\circ} T(d_{b}).
\end{array}$$

The verification of the comonoid properties involves lengthy
calculations, which are basically straightforward. We just show that
$u$ is neutral element for $d$, using the equations from
Definition~\ref{BasisDef}.
$$\begin{array}{rcl}
\lefteqn{(u_{b}\otimes\idmap) \mathrel{\circ} d_{d}} \\
& = &
(T(!)\otimes\idmap) \mathrel{\circ} (b\otimes\idmap) \mathrel{\circ} (a \otimes a)
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes\idmap) \mathrel{\circ} (\mu\otimes\idmap) \mathrel{\circ} (T(b)\otimes a)
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes T(a)) \mathrel{\circ} (T(b)\otimes T(b))
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(b\otimes b) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(\eta\times \eta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ} (T(\eta)\times T(\eta)) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(T(!)\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} (T(!)\otimes \idmap) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(!\times \idmap)
   \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(\idmap\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\lambda^{-1}) \mathrel{\circ} b
   \qquad \mbox{where }\lambda\colon 1\times X \congrightarrow X \\
& = &
(\idmap\otimes a) \mathrel{\circ} \lambda^{-1} \mathrel{\circ} b
   \qquad \mbox{since $\xi$ is monoidal, where $\lambda \colon
   I \otimes X  \congrightarrow X$} \\
& = &
\lambda^{-1} \mathrel{\circ} a \mathrel{\circ} b \\
& = &
\lambda^{-1}.
\end{array}$$

Associativity:
$$\begin{array}{rcl}
\lefteqn{\alpha \mathrel{\circ} (\idmap\otimes d) \mathrel{\circ} d} \\
& = &
\alpha \mathrel{\circ} (\idmap \otimes (a \otimes a)) \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\idmap \otimes b) \mathrel{\circ} \\
& & \qquad
   (a \otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
\alpha \mathrel{\circ} (a \otimes (a \otimes a)) \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\idmap \otimes \mu) \mathrel{\circ} \\
& & \qquad
   (\idmap \otimes T(b)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
\alpha \mathrel{\circ} (a \otimes (a \otimes a)) \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (T(a) \otimes \mu) \mathrel{\circ} \\
& & \qquad
   (T(b) \otimes T(b)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
\alpha \mathrel{\circ} (a \otimes (a \otimes a)) \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\mu \otimes \mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(b \times b) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\mu \otimes \mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\mu \otimes \mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\mu \otimes \mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\eta\times\eta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} (\mu \otimes \mu) \mathrel{\circ} \\
& & \qquad
   (T(\eta)\otimes T(\eta)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} (\idmap \otimes T(\Delta)) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} \alpha \mathrel{\circ} (\idmap \otimes \xi^{-1})
   \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\idmap \times \Delta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1} \otimes \idmap) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\alpha) \mathrel{\circ} T(\idmap \times \Delta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1} \otimes \idmap) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta \times \idmap) \mathrel{\circ} T(\Delta) \mathrel{\circ} b.
\end{array}$$

\noindent In a similar way one obtains the same outcome by starting from:
$$\begin{array}{rcl}
(d\otimes\idmap) \mathrel{\circ} d
& = &
((a \otimes a) \otimes\idmap) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (b\otimes\idmap) \mathrel{\circ} \\
& & \qquad
   (a \otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\idmap) \mathrel{\circ} \\
& & \qquad
   (T(b)\otimes\idmap) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes T(a )) \mathrel{\circ} \\
& & \qquad
   (T(b)\otimes T(b)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(b\times b) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\eta\times \eta) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} (\mu\otimes\mu) \mathrel{\circ} \\
& & \qquad
   (T(\eta)\otimes T(\eta)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1}\otimes\idmap)
   \mathrel{\circ} (T(\Delta)\otimes\idmap) \mathrel{\circ} \\
& & \qquad
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
((a \otimes a) \otimes a) \mathrel{\circ} (\xi^{-1} \otimes \idmap) \mathrel{\circ} \xi^{-1}
   \mathrel{\circ} T(\Delta \times \idmap) \mathrel{\circ} T(\Delta) \mathrel{\circ} b.
\end{array}$$

\noindent This comultiplication $d$ is commutative:
$$\begin{array}{rcl}
\gamma \mathrel{\circ} d
& = &
\gamma \mathrel{\circ} (a \otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(a \otimes a) \mathrel{\circ} \gamma \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(a \otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\gamma) \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(a \otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
d.
\end{array}$$

For functoriality, assume two algebras $\smash{T(X_{i})
  \stackrel{a_i}{\rightarrow} X_{i}}$, for $i=1,2$, carrying
$\smash{\overline{T}}$-coalgebras $X_{i} \stackrel{b_i}{\rightarrow}
T(X_{i})$. A map of coalgebras $f\colon b_{1} \rightarrow b_{2}$ is
given by a map $f\colon X_{1} \rightarrow X_{2}$ satisfying $f \mathrel{\circ}
a_{1} = a_{2} \mathrel{\circ} T(f)$ and $b_{2} \mathrel{\circ} f = T(f) \mathrel{\circ} b_{1}$.
This $f$ is then a map $(d_{1},u_{1}) \rightarrow (d_{2}, u_{2})$
between the induced comonoid. For instance,
$$u_{2} \mathrel{\circ} f
=
F(!) \mathrel{\circ} b_{2} \mathrel{\circ} f
=
F(!) \mathrel{\circ} T(f) \mathrel{\circ} b_{1}
=
F(!) \mathrel{\circ} b_{1}
=
u_{1}.\eqno{\qEd}$$

$$\begin{array}{rcl}
d_{2} \mathrel{\circ} f
& = &
(a_{2} \otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b_{2}
   \mathrel{\circ} f \\
& = &
(a_{2} \otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(f)
   \mathrel{\circ} b_{1} \\
& = &
(a_{2} \otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(f\times f) \mathrel{\circ} T(\Delta)
   \mathrel{\circ} b_{1} \\
& = &
(a_{2} \otimes a_{2}) \mathrel{\circ} (T(f)\otimes T(f)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta)
   \mathrel{\circ} b_{1} \\
& = &
(f \otimes f) \mathrel{\circ} (a_{1}\otimes a_{1}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta)
   \mathrel{\circ} b_{1} \\
& = &
(f \otimes f) \mathrel{\circ} d_{1}.
\end{array}$$

It is not hard to see that when the monoidal structure on $\cat{A}$ is
cartesian, applying the constructions~(\ref{ComonoidDefEqn}) to the
coalgebra $\delta = T(\eta) \colon T(Y)\rightarrow T^{2}(X)$ on a free
algebra $T(Y)$, as in Lemma~\ref{FreeAlgCoalgLem}, yields essentially
this comonoid:
\begin{equation}
\label{FreeAlgCoalgComonoidDiag}
\vcenter{\xymatrix{
T(1) & & T(Y)\ar[ll]_-{u = T(!)}\ar[rr]^-{d = \xi^{-1} \mathrel{\circ} T(\Delta)}
   & & T(Y)\otimes T(Y)
}}
\end{equation}

The unit is obtained as $u = T(!) \mathrel{\circ} \delta = T(!) \mathrel{\circ} T(\eta)
= T(! \mathrel{\circ} \eta) = T(!)$, and the comultiplication as:
$$\begin{array}{rcl}
d
& = &
(\mu \otimes\mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} \delta \\
& = &
(\mu \otimes\mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(\eta) \\
& = &
(\mu \otimes\mu) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\eta\times\eta) \mathrel{\circ} T(\Delta) \\
& = &
(\mu \otimes\mu) \mathrel{\circ} (T(\eta)\otimes T(\eta)) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(\Delta) \\
& = &
\xi^{-1} \mathrel{\circ} T(\Delta).
\end{array}$$
}

\begin{exa}
\label{ComonoidEx}
To make the comonoid construction~(\ref{ComonoidDefEqn}) more
concrete, let $V$ be a vector space, say over the complex numbers
$\mathbb{C}$, with a Hamel basis, described as a coalgebra $b\colon
V\rightarrow \ensuremath{\mathcal{M}}_{\mathbb{C}}(V)$ like in
Theorem~\ref{OperatorCoalgThm}, with basic elements $(e_{j})$,
satisfying $b(e_{j}) = 1e_{j}$. The counit $u_{b} =
\ensuremath{\mathcal{M}}_{\mathbb{C}}(!)  \mathrel{\circ} b \colon V\rightarrow \mathbb{C}$
from~\eqref{ComonoidDefEqn} first represents a vector wrt.\ this
basis, and then adds the (finitely many) coefficients:
$$\textstyle v
\longmapsto
\sum_{j}v_{j}e_{j}
\longmapsto
\sum_{j}v_{j}.$$

\noindent Similarly, the comultiplication $d_{b} \colon V \rightarrow
V\otimes V$ as in~\eqref{ComonoidDefEqn} is the composite:
$$\textstyle v
\longmapsto
\sum_{j}v_{j}e_{j}
\longmapsto
\sum_{j}v_{j}(e_{j}\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}} e_{j}),$$

\noindent like in~\cite{CoeckePV12}.

(For Hilbert spaces one uses orthonormal bases instead of Hamel bases;
the counit $u$ of the comonoid then exists only in the
finite-dimensional case. The comultiplication $d$ seems more relevant,
see also below, and may thus also be studied on its own, like
in~\cite{AbramskyH12}, without finiteness restriction.)

Another example is the ideal monad $\textsl{Idl}\xspace\colon\Cat{PoSets}\xspace \rightarrow
\Cat{PoSets}\xspace$ from Subsection~\ref{DcpoSubsec}. It preserves finite
products, and as a result, the induced monoidal structure on the
category of algebras $\textsl{Alg}\xspace(\textsl{Idl}\xspace) = \Cat{Dcpo}$ is cartesian. Hence the
comonoid structure~(\ref{ComonoidDefEqn}) is given by actual diagonals
and (unique) maps to the final object. For instance, when $\otimes =
\times$ on algebras:
$$\begin{array}{rcll}
d
& = &
(a\times a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \\
& = &
(a\times a) \mathrel{\circ} \Delta \mathrel{\circ} b &
   \quad \mbox{since } \xi^{-1} = \tuple{T(\pi_{1}), T(\pi_{2})} \\
& = &
\Delta \mathrel{\circ} a \mathrel{\circ} b \\
& = &
\Delta.
\end{array}$$
\end{exa}

\noindent In general, given a comonoid $\smash{I\stackrel{u}{\leftarrow} X
  \stackrel{d}{\rightarrow} X\otimes X}$, an endomap $f\colon
X\rightarrow X$ may be called \emph{diagonalised}---wrt.~this
comonoid, or actually, comultiplication $d$---if there is a ``map of
eigenvalues'' $v\colon X\rightarrow I$ such that $f$ equals the
composite:
\begin{equation}
\label{ComonoidDiagEqn}
\vcenter{\xymatrix{
X\ar[r]^-{d} & X\otimes X\ar[r]^-{v\otimes\idmap} &
   I\otimes X\ar[r]^-{\lambda}_-{\cong} & X.
}}
\end{equation}

\noindent In case the diagonal $d$ is part of a comonoid, with a
counit $u\colon X \rightarrow I$, then this eigenvalue map $v$ equals
$u \mathrel{\circ} f$.

\auxproof{
Assume $f$ is diagonalised as above. Then:
$$\begin{array}{rcl}
u \mathrel{\circ} f
& = &
u \mathrel{\circ} \lambda_{X} \mathrel{\circ} (v\otimes\idmap) \mathrel{\circ} d \\
& = &
\lambda_{I} \mathrel{\circ} (\idmap\otimes v) \mathrel{\circ} (v\otimes\idmap) \mathrel{\circ} d \\
& = &
\rho_{I} \mathrel{\circ} (v\otimes\idmap) \mathrel{\circ} (\idmap\otimes v) \mathrel{\circ} d \\
& = &
\rho_{I} \mathrel{\circ} (v\otimes\idmap) \mathrel{\circ} \rho_{X}^{-1} \\
& = &
v.
\end{array}$$
}

In the special case where the comonoid comes from a
coalgebra (basis) $b\colon X\rightarrow T(X)$, like
in~(\ref{ComonoidDefEqn}), an endomap of algebras $f\colon
X\rightarrow X$, say on $a\colon T(X)\rightarrow X$, is diagonalised
if there is a map of algebras $v\colon X\rightarrow I = T(1)$ such
that $f$ is:
$$\vcenter{\xymatrix@C-.5pc{
X\ar[r]^-{b} &
T(X)\ar[rr]^-{T(\tuple{v,\idmap})} & &
T(T(1)\times X)\ar[r]^-{T(\ensuremath{\mathsf{st}})} &
T^{2}(1\times X) \ar[r]^-{\cong} &
T^{2}(X)\ar[r]^-{\mu} &
T(X)\ar[r]^-{a} &
X,
}}$$

\noindent where $\ensuremath{\mathsf{st}}$ is a strength map of the form $T(X)\times Y
\rightarrow T(X\times Y)$, which exists because the monad $T$ is
assumed to be commutative.

\begin{exa}
\label{BifMRelEx}
Recall the multiset monad $\ensuremath{\mathcal{M}}_S$ from
Subsection~\ref{VectorSpaceSubsec}, where $S$ is a semiring.
In~\cite{Jacobs11a} it is used to defined a dagger category
$\Cat{BifMRel}\xspace_S$ of ``bifinite multirelations''.  Objects are sets $X$,
and maps $X \rightarrow Y$ in $\Cat{BifMRel}\xspace_S$ are multirelations $r\colon
X\times Y \rightarrow S$ which factor both as
$X\rightarrow\ensuremath{\mathcal{M}}_{S}(Y)$ and as $Y\rightarrow\ensuremath{\mathcal{M}}_{S}(X)$. This means
that for each $x$ there are finitely many $y$ with $r(x,y)\neq 0$, and
similarly, for each $y$ there are finitely many $x$ with $r(x,y)\neq
0$. Composition of $r\colon X\rightarrow Y$ and $s\colon Y\rightarrow
Z$ is done via matrix multiplication: $(s\mathrel{\circ} r)(x,z) = \sum_{y}
s(y,z)\cdot r(x,y)$. The identity $\idmap\colon X \rightarrow X$ is
the given by $\idmap(x,x) = 1$ and $\idmap(x,x')=0$ if $x\neq x'$.

Here we don't need the dagger $(-)^{\dag}$ on $\Cat{BifMRel}\xspace_{S}$, but for
completeness we briefly mention how it arises, assuming that $S$
carries an involution $\overline{(-)}\colon S\rightarrow S$, like
conjugation on the complex numbers. For a map $r\colon X\rightarrow Y$
there is an associated map $r^{\dag}\colon Y\rightarrow X$ in the
reverse direction, obtained by swapping arguments and involution:
$r^{\dag}(y,x) = \overline{r(x,y)}$, like in a conjugate
transpose. This makes $\Cat{BifMRel}\xspace_{S}$ a dagger category.

The category $\Cat{BifMRel}\xspace_{S}$ is symmetric monoidal, with $\times$ as
tensor and $1 = \{*\}$ as tensor unit. Coproducts $(+,0)$ give
biproducts. Interestingly, each object $X$ carries a (canonical)
diagonal $d\colon X \rightarrow X\otimes X$ given by:
$$\xymatrix{
X\times (X\times X)\ar[r]^-{d} & S,
\qquad
(x,(y,y'))\ar@{|->}[r] & {\left\{\begin{array}{ll}
   1 & \mbox{ if }x=y=y' \\ 0 & \mbox{ otherwise.} \end{array}\right.}
}$$

\noindent There is in general no associated counit $u\colon X
\rightarrow 1$.

Now let's see what it means that a map $r\colon X\rightarrow X$ in
$\Cat{BifMRel}\xspace_{S}$ is diagonalised wrt.\ this $d$. It would require an
eigenvalue map $v\colon X \rightarrow 1$, that is, a function $v\colon
X \rightarrow S$ in $\Cat{Sets}\xspace$, so that $r\colon X \times X \rightarrow S$
satisfies:
$$\begin{array}{rcl}
r(x,x')
& = &
\left\{\begin{array}{ll}
v(x) & \mbox{ if }x=x' \\
0 & \mbox{ otherwise.}
\end{array}\right.
\end{array}$$

\noindent Hence such a diagonalised map is a diagonal matrix.
\end{exa}

What precisely is a diagonalised form depends on the diagonalisation
(comonoid) map $d$ involved. This is clear in the following example,
involving Pauli matrices.

\begin{exa}
\label{PauliEx}
We consider the set $\mathbb{C}^{2}$ as vector space over
$\mathbb{C}$, and thus as algebra of the (commutative) multiset monad
$\ensuremath{\mathcal{M}}_{\mathbb{C}}\colon \Cat{Sets}\xspace \rightarrow \Cat{Sets}\xspace$ via the map
$\smash{\ensuremath{\mathcal{M}}_{\mathbb{C}}(\mathbb{C}^{2})
  \stackrel{a}{\longrightarrow} \mathbb{C}^{2}}$ that sends a formal
sum $s_{1}(z_{1}, w_{1}) + \cdots + s_{n}(z_{n}, w_{n})$ of pairs in
$\mathbb{C}^{2}$ to the pair of sums $(s_{1}\cdot z_{1} + \cdots +
s_{n}\cdot z_{n}, s_{1}\cdot w_{1} + \cdots + s_{n}\cdot w_{n})
\in\mathbb{C}^{2}$.

The familiar Pauli spin functions $\sigma_{\textsf{x}},
\sigma_{\textsf{y}}, \sigma_{\textsf{z}} \colon \mathbb{C}^{2}
\rightarrow \mathbb{C}^{2}$ are given by:
$$\sigma_{\textsf{x}}(z,w) = (w,z)
\qquad\quad
\sigma_{\textsf{y}}(z,w) = (-iw, iz)
\qquad\quad
\sigma_{\textsf{z}}(z,w) = (z,-w).$$

\noindent We concentrate on $\sigma_{\textsf{x}}$; it satisfies
$\sigma_{\textsf{x}}(1,1) = (1,1)$ and $\sigma_{\textsf{x}}(1,-1) =
-(1,-1)$. These eigenvectors $(1,1)$ and $(1,-1)$ are organised in a
basis $b_{\textsf{x}}\colon \mathbb{C}^{2} \rightarrow
\ensuremath{\mathcal{M}}_{\mathbb{C}}(\mathbb{C}^{2})$, as in Definition~\ref{BasisDef},
via the following formal sum.
$$\begin{array}{rcl}
b_{\textsf{x}}(z,w)
& = &
\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1).
\end{array}$$

\noindent It expresses an arbitrary element of
$\mathbb{C}^{2}$ in terms of this basis of eigenvectors. It is not
hard to see that $b_{\textsf{x}}$ is a
$\overline{\ensuremath{\mathcal{M}}_{\mathbb{C}}}$-coalgebra; for instance:
$$\textstyle\big(a \mathrel{\circ} b_{\textsf{x}})(z,w)
=
a\big(\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1)\big)
=
(\frac{z+w}{2} + \frac{z-w}{2}, \frac{z+w}{2} - \frac{z-w}{2})
=
(z,w).$$

\auxproof{
$$\begin{array}{rcl}
\big(\ensuremath{\mathcal{M}}_{\mathbb{C}}(b_{\textsf{x}}) \mathrel{\circ} b_{\textsf{x}}\big)(z,w)
& = &
\frac{z+w}{2}b_{\textsf{x}}(1,1) + \frac{z-w}{2}b_{\textsf{x}}(1,-1) \\
& = &
\frac{z+w}{2}\big((1(1,1) + 0(1,-1)\big) +
   \frac{z-w}{2}\big(0(1,1) + 1(1,-1)\big) \\
& = &
\frac{z+w}{2}\big((1(1,1)\big) + \frac{z-w}{2}\big(1(1,-1)\big) \\
& = &
\frac{z+w}{2}\big(\eta(1,1)\big) + \frac{z-w}{2}\big(\eta(1,-1)\big) \\
& = &
\big(\ensuremath{\mathcal{M}}_{\mathbb{C}}(\eta) \mathrel{\circ} b_{\textsf{x}}\big)(z,w) \\
& = &
\big(\delta \mathrel{\circ} b_{\textsf{x}}\big)(z,w).
\end{array}$$

We also check that $b_{\textsf{x}}$ is a map of algebras:
$$\begin{array}{rcl}
\lefteqn{\textstyle\big(\mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}(b_{\textsf{x}})\big)
   (\sum_{j}s_{j}(z_{j},w_{j}))} \\
& = &
\mu(\sum_{j}s_{j}b_{\textsf{x}}(z_{j},w_{j})) \\
& = &
\mu(\sum_{j}s_{j}(\frac{z_{j}+w_{j}}{2}(1,1) + \frac{z_{j}-w_{j}}{2}(1,-1))) \\
& = &
\sum_{j}(s_{j}\cdot\frac{z_{j}+w_{j}}{2})(1,1) +
   (s_{j}\cdot\frac{z_{j}-w_{j}}{2})(1,-1) \\
& = &
\sum_{j}\frac{s_{j}\cdot z_{j}+s_{j}\cdot w_{j}}{2}(1,1) +
   \sum_{j}\frac{s_{j}\cdot z_{j}-s_{j}\cdot w_{j}}{2}(1,-1) \\
& = &
{\displaystyle
\frac{(\sum_{j}s_{j}\cdot z_{j})+(\sum_{j}s_{j}\cdot w_{j})}{2}(1,1) +
   \frac{(\sum_{j}s_{j}\cdot z_{j})-(\sum_{j}s_{j}\cdot w_{j})}{2}(1,-1)} \\
& = &
b_{\textsf{x}}(\sum_{j}s_{j}\cdot z_{j}, \sum_{j}s_{j}\cdot w_{j}) \\
& = &
\big(b_{\textsf{x}} \mathrel{\circ} a\big)(\sum_{j}s_{j}(z_{j},w_{j})).
\end{array}$$

The equaliser~(\ref{BasisEqualiserDiag}) for the basic elements
yields the expected outcome:
$$\begin{array}{rcl}
X_{b}
& = &
\set{(z,w)}{b_{\textsf{x}}(z,w) = \eta(z,w)} \\
& = &
\set{(z,w)}{\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1) = 1(z,w)} \\
& = &
\{(1,1), (1,-1)\}.
\end{array}$$
}

\noindent The comonoid structure $\smash{\mathbb{C}
  \xleftarrow{u_{\textsf{x}}} \mathbb{C}^{2}
  \xrightarrow{d_{\textsf{x}}} \mathbb{C}^{2}\otimes \mathbb{C}^{2}}$
induced by $b_{\textsf{x}}$ as in~(\ref{ComonoidDefEqn}) is given by
$u_{\textsf{x}}(z,w) = z$ and $d_{\textsf{x}}(z,w) =
\frac{z+w}{2}\big((1,1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,1)\big) +
\frac{z-w}{2}\big((1,-1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,-1)\big)$. The eigenvalue map
$v_{\textsf{x}}\colon \mathbb{C}^{2} \rightarrow \mathbb{C}$ is given
by $v_{\textsf{x}}(z,w) = w$. The eigenvalues $1,-1$ appear by
application to the basic elements: $v_{\textsf{x}}(1,1) = 1$ and
$v_{\textsf{x}}(1,-1) = -1$. Further, the Pauli function
$\sigma_{\textsf{x}}$ is diagonalised as in~(\ref{ComonoidDiagEqn})
via these $d_{\textsf{x}}, v_{\textsf{x}}$, since:
$$\begin{array}{rcl}
\lefteqn{\big(\lambda \mathrel{\circ} (v_{\textsf{x}}\otimes\idmap) \mathrel{\circ}
   d_{\textsf{x}}\big)(z,w)} \\
& = &
\big(\lambda \mathrel{\circ} (v_{\textsf{x}}\otimes\idmap)\big)
   \Big(\frac{z+w}{2}\big((1,1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,1)\big) +
    \frac{z-w}{2}\big((1,-1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,-1)\big)\Big) \\
& = &
\lambda\Big(\frac{z+w}{2}\big(1\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,1)\big) +
    \frac{z-w}{2}\big(-1\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,-1)\big)\Big) \\
& = &
\frac{z+w}{2}(1,1) - \frac{z-w}{2}(1,-1) \\
& = &
(w, z) \\
& = &
\sigma_{\textsf{x}}(z,w).
\end{array}$$

\auxproof{
$$\begin{array}{rcl}
u_{\textsf{x}}(z,w)
& = &
\big(\ensuremath{\mathcal{M}}_{\mathbb{C}}(!) \mathrel{\circ} b_{\textsf{x}}\big)(z,w) \\
& = &
\ensuremath{\mathcal{M}}_{\mathbb{C}}(!)\Big(\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1)\Big) \\
& = &
\frac{z+w}{2} + \frac{z-w}{2} \\
& = &
z \\
d_{\textsf{x}}(z,w)
& = &
\big((a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}(\Delta)
   \mathrel{\circ} b_{\textsf{x}}\big)(z,w) \\
& = &
\big((a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}(\Delta)\big)
   \Big(\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1)\Big) \\
& = &
\big((a\otimes a) \mathrel{\circ} \xi^{-1}\big)
   \Big(\frac{z+w}{2}\tuple{(1,1),(1,1)} +
      \frac{z-w}{2}\tuple{(1,-1),(1,-1)}\Big) \\
& = &
\big(a\otimes a\big)
   \Big(\frac{z+w}{2}\big((1,1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,1)\big) +
      \frac{z-w}{2}\big((1,-1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,-1)\big)\Big) \\
& = &
\frac{z+w}{2}\big((1,1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,1)\big) +
    \frac{z-w}{2}\big((1,-1)\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}(1,-1)\big).
\end{array}$$

Alternatively, elaborating the formula~(\ref{AlgDiagEqn}) yields:
$$\begin{array}{rcl}
\lefteqn{\big(a \mathrel{\circ} \mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}^{2}(\pi_{1}) \mathrel{\circ}
   \ensuremath{\mathcal{M}}_{\mathbb{C}}(\ensuremath{\mathsf{st}}) \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}(\tuple{\idmap,\lambda})
   \mathrel{\circ} b\big)(z,w)} \\
& = &
\big(a \mathrel{\circ} \mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}^{2}(\pi_{1}) \mathrel{\circ}
   \ensuremath{\mathcal{M}}_{\mathbb{C}}(\ensuremath{\mathsf{st}}) \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}(\tuple{\idmap,\lambda})\big)
   \big(\frac{z+w}{2}(1,1) + \frac{z-w}{2}(1,-1)\big) \\
& = &
\big(a \mathrel{\circ} \mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}^{2}(\pi_{1}) \mathrel{\circ}
   \ensuremath{\mathcal{M}}_{\mathbb{C}}(\ensuremath{\mathsf{st}})\big)
   \big(\frac{z+w}{2}\tuple{\idmap,\lambda}(1,1) +
   \frac{z-w}{2}\tuple{\idmap,\lambda}(1,-1)\big) \\
& = &
\big(a \mathrel{\circ} \mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}^{2}(\pi_{1})\big)
   \big(\frac{z+w}{2}\ensuremath{\mathsf{st}}(\tuple{(1,1), 1*}) +
   \frac{z-w}{2}\ensuremath{\mathsf{st}}(\tuple{(1,-1), -1*})\big) \\
& = &
\big(a \mathrel{\circ} \mu \mathrel{\circ} \ensuremath{\mathcal{M}}_{\mathbb{C}}^{2}(\pi_{1})\big)
   \big(\frac{z+w}{2}(1\tuple{(1,1), *}) +
   \frac{z-w}{2}(-1\tuple{(1,-1), *})\big) \\
& = &
\big(a \mathrel{\circ} \mu\big) \big(\frac{z+w}{2}(1(1,1)) +
   \frac{z-w}{2}(-1(1,-1))\big) \\
& = &
a\big(\frac{z+w}{2}(1,1) + \frac{w-z}{2}(1,-1)\big) \\
& = &
(\frac{z+w}{2} + \frac{w-z}{2}, \frac{z+w}{2} - \frac{w-z}{2}) \\
& = &
(w, z) \\
& = &
\sigma_{\textsf{x}}(z,w).
\end{array}$$
}

\noindent In a similar way one defines for the other Pauli functions
$\sigma_{\textsf{y}}$ and $\sigma_{\textsf{z}}$:
$$\begin{array}{rclcrcl}
b_{\textsf{y}}(z,w)
& = &
\frac{iz+w}{2}(-i,1) + \frac{iz-w}{2}(i,1)
& \qquad &
v_{\textsf{y}}(z,w)
& = &
iz \\
b_{\textsf{z}}(z,w)
& = &
z(1,0) - w(0,1)
& \qquad &
v_{\textsf{z}}(z,w)
& = &
z-w.
\end{array}$$

\end{exa}

\noindent The situation that we have is similar to what one finds in categorical
models of linear logic, where the exponential $!A$, giving arbitrarily
many copies of $A$, is interpreted via a comonad $!$ carrying a
comonoid structure $!A \leftarrow\, !A\otimes !A \rightarrow I$ for
weakening and contraction. In the current situation we have a basis as
a coalgebra $A\rightarrow\, !A$, so that we get a comonoid structure
on $A$, instead of on $!A$.

The next result can be interpreted informally as: base vectors are
copyable.

\begin{prop}
\label{BaseCopyProp}
Assume an algebra $\smash{T(X)\stackrel{a}{\rightarrow} X}$ with an
`element' $\smash{I\stackrel{x}{\rightarrow} X}$ in $\textsl{Alg}\xspace(T)$ that is
in the basis of a coalgebra $b\colon X\rightarrow T(X)$, as in the
equaliser diagram~(\ref{BasisEqualiserDiag}):
$$\xymatrix@C+0.5pc@R-1pc{
X_{b}\ar@{ >->}[r]^-{e} & X \ar@<+.5ex>[r]^-{b}\ar@<-.5ex>[r]_-{\eta} & T(X) \\
I\ar@{-->}[u]\ar[ur]_{x}
}$$

\noindent This $x$ is then copyable, in the sense that the
following diagram commutes
$$\xymatrix@R-1pc{
I\ar[r]^-{x}\ar[d]_{\cong} & X\ar[d]^{d} \\
I\otimes I\ar[r]_-{x\otimes x} & X\otimes X
}$$

\noindent where $d$ is the comultiplication associated with $b$
as in~(\ref{ComonoidDefEqn}).
\end{prop}

\begin{myproof}
Since $I = T(1)$ is a free algebra, the map of algebras $x\colon
I\rightarrow X$ can be written as $x = a \mathrel{\circ} T(x')$, for the
element $x' = x \mathrel{\circ} \eta \colon 1 \rightarrow X$ in the underlying
category. Then:
$$\begin{array}{rcll}
b \mathrel{\circ} x
\hspace*{\arraycolsep} = \hspace*{\arraycolsep}
b \mathrel{\circ} a \mathrel{\circ} T(x')
& = &
\mu \mathrel{\circ} T(b) \mathrel{\circ} T(x \mathrel{\circ} \eta)
   & \mbox{see Definition~\ref{BasisDef}} \\
& = &
\mu \mathrel{\circ} T(\eta) \mathrel{\circ} T(x \mathrel{\circ} \eta) \quad
   & \mbox{since $x$ is in the basis $X_b$} \\
& = &
T(x \mathrel{\circ} \eta) \\
& = &
T(x').
\end{array}$$

\noindent Now we use that $\xi$ is a monoidal isomorphism in:
$$\xymatrix@R-1pc{
\llap{$I=\;$}T(1)\ar[d]_{\rho}^{\cong}
   \ar@/^2ex/[rd]^-{T(\rho) = T(\Delta)} \\
T(1)\otimes T(1)\ar[r]_-{\xi}^-{\cong} & T(1\times 1)
}$$

\noindent in order to prove that $x$ is copyable:
$$\begin{array}[b]{rcll}
(x\otimes x) \mathrel{\circ} \rho
& = &
(a\otimes a) \mathrel{\circ} (T(x')\otimes T(x')) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1}  \mathrel{\circ} T(x'\times x')\mathrel{\circ} T(\Delta) \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} T(x') \\
& = &
(a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} b \mathrel{\circ} x
   & \mbox{as just shown} \\
& = &
d \mathrel{\circ} x & \mbox{with $d$ as in~(\ref{ComonoidDefEqn}).}
\end{array}\eqno{\qEd}$$
\end{myproof}

\noindent The converse of this result is not true: for the ideal monad in
Example~\ref{ComonoidEx} every element is copyable, but not every
element is compact, \textit{i.e.}~in a basis, see
Subsection~\ref{DcpoSubsec}.

Comonoids make tensors cartesian, see~\cite{Fox76,CoeckeP08}, so
that they bring us into the classical world. This cartesian structure
already exists for coalgebras, as the next result shows.

\begin{prop}
\label{CoalgComonoidProductProp}
The comonoid structure~(\ref{ComonoidDefEqn}) restricts to a comonoid
in the category $\smash{\textsl{CoAlg}\xspace(\overline{T})}$ of bases. Therefore, this
category has finite products.  Moreover, the restriction of the free
functor $F\colon \cat{A} \rightarrow \textsl{Alg}\xspace(T)$ to $F\colon \cat{A}
\rightarrow \textsl{CoAlg}\xspace(\overline{T})$, as in Lemma~\ref{FreeAlgCoalgLem},
preserves finite products.
\end{prop}

\begin{myproof}
First one checks that the maps $d,u$ in~(\ref{ComonoidDefEqn}) are
homomorphisms of coalgebras. Then one uses that the comonad
$\smash{\overline{T}} \colon \textsl{Alg}\xspace(T) \rightarrow \textsl{Alg}\xspace(T)$ is monoidal,
see~\cite[Prop.~5.7]{Jacobs94a}, so that the products of coalgebras
can be defined as:
$$\begin{array}{rclcrcl}
1
& = &
\left(\vcenter{\xymatrix@R-1.3pc{
T^{2}(1) \\
T(1)\ar[u]_{\delta}
}}\right)
& \qquad\quad &
\left(\vcenter{\xymatrix@R-1.3pc{
\overline{T}(X_{1}) \\
X_{1}\ar[u]_{b_1}
}}\right)
\times
\left(\vcenter{\xymatrix@R-1.3pc{
\overline{T}(X_{2}) \\
X_{2}\ar[u]_{b_2}
}}\right)
& = &
\left(\vcenter{\xymatrix@R-1.3pc{
\overline{T}(X_{1}\otimes X_{2}) \\
\overline{T}(X_{1})\otimes \overline{T}(X_{2})\ar[u] \\
X_{1}\otimes X_{2}\ar[u]_{b_{1}\otimes b_{2}}
}}\right)
\end{array}$$

\noindent where on the right-hand-side we use the map:
$$\xymatrix{
FU(X_{1})\otimes FU(X_{2}) \ar[r]^-{\xi}_-{\cong} &
   F\big(U(X_{1})\otimes U(X_{2})\big)\ar[r]^-{F(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}})} &
   FU(X_{1}\otimes X_{2}),
}$$

\noindent in which $\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}$ is the universal bi-homomorphism. \qed
\end{myproof}

\auxproof{
Given a coalgebra $b\colon X\rightarrow \overline{T}(X)$ on $a\colon T(X)
\rightarrow X$, the unit map $u_{b} = T(!) \mathrel{\circ} b \colon X \rightarrow T(1)$
is a map of algebras \& coalgebras:
$$\begin{array}{rcl}
\mu \mathrel{\circ} T(u_{b})
& = &
\mu \mathrel{\circ} T(T(!) \mathrel{\circ} b) \\
& = &
T(!) \mathrel{\circ} \mu \mathrel{\circ} T(b) \\
& = &
T(!) \mathrel{\circ} b \mathrel{\circ} a \\
& = &
u_{b} \mathrel{\circ} a \\
\delta \mathrel{\circ} u_{b}
& = &
\delta \mathrel{\circ} T(!) \mathrel{\circ} b \\
& = &
T^{2}(!) \mathrel{\circ} \delta \mathrel{\circ} b \\
& = &
T^{2} \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
T(T(!) \mathrel{\circ} b) \mathrel{\circ} b \\
& = &
T(u_{b}) \mathrel{\circ} b.
\end{array}$$

\noindent Moreover, it is the unique one, since if $f\colon
X\rightarrow T(1)$ is also a map of $\overline{T}$-coalgebras, then it
is a map of comonoids, by Proposition~\ref{CoalgComonoidProp}, and
thus:
$$\begin{array}{rcl}
f
& = &
\idmap[T(1)] \mathrel{\circ} f \\
& = &
u_{T(1)} \mathrel{\circ} f \qquad \mbox{by~(\ref{FreeAlgCoalgComonoidDiag})} \\
& = &
u_{b} \\
& = &
T(!) \mathrel{\circ} b.
\end{array}$$

We turn to products, and define projections:
$$\xymatrix{
\pi_{1} = \Big(X_{1}\otimes X_{2}\ar[r]^-{\idmap\otimes u_{2}} &
   X_{1}\otimes T(1)\ar[r]^-{\rho}_-{\cong} & X_{1}\Big)
}$$

\noindent and similarly for $\pi_2$. This gives maps of algebras,
by construction:
$$\xymatrix@R-1pc@C+1pc{
T(X_{1}\otimes X_{2})\ar[d]_{a_{1}\otimes a_{2}}\ar[r]^-{T(\idmap\otimes u_{2})} &
   T(X_{1}\otimes T(1))\ar[d]^{a_{1}\otimes \mu_{1}}\ar[r]^-{T(\rho)} &
   T(X_{1})\ar[d]^{a_{1}} \\
X_{1}\otimes X_{2}\ar[r]_-{\idmap\otimes u_{2}} &
   X_{1}\otimes T(1)\ar[r]_-{\rho} & X_{1}
}$$

\noindent where we have overloaded the $\otimes$-notation. It is
also a map of coalgebras:
$$\begin{array}{rcl}
T(\pi_{1}) \mathrel{\circ} (b_{1}\times b_{2})
& = &
T(\rho) \mathrel{\circ} T(\idmap\otimes u_{2}) \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
T(\rho) \mathrel{\circ} \xi \mathrel{\circ} (\idmap\otimes T(u_{2})) \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
T(\rho) \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes \delta_{1}) \mathrel{\circ}
   (\idmap\otimes u_{2}) \\
& = &
\rho \mathrel{\circ} (b_{1}\otimes \delta_{1}) \mathrel{\circ} (\idmap\otimes u_{2}) \\
& = &
b_{1} \mathrel{\circ} \rho \mathrel{\circ} (\idmap\otimes u_{2}) \\
& = &
b_{1} \mathrel{\circ} \pi_{1}
\end{array}$$

Next, assume homomorphisms $f_{i} \colon b \rightarrow b_{i}$. Take as
tuple $\tuple{f_{1}, f_{2}} = (f_{1}\otimes f_{2}) \mathrel{\circ} d_{b} \colon
X \rightarrow X_{1}\otimes X_{2}$. We need to check that
comultiplications $d$ are maps of coalgebras $b\rightarrow
b\otimes b$. This requires some care, and a better understanding of
the monoidal transformations involved. We recall that the map $\xi
\colon FA \otimes FB \congrightarrow F(A \times B)$, for $A,B\in\cat{A}$,
is obtained in:
$$\xymatrix{
T(X)\times T(Y)\ar[rr]^-{\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}} = t\mathrel{\circ} \eta}\ar[drr]_{\ensuremath{\mathsf{dst}} = \xi^T} & &
   T(X)\otimes T(Y)\ar@{-->}[d]^{\xi}_{\cong} \\
& & T(X\times Y)
}$$

\noindent with inverse for $\xi$ given by:
$$\xymatrix{
\sigma \stackrel{\textrm{def}}{=} \Big(T(X\times Y)\ar[r]^{T(\eta\times\eta)} &
   T(T(X)\times T(Y))\ar[r]^-{t} & T(X)\otimes T(Y)\Big).
}$$

\noindent The map $\varphi\colon \overline{T}(X_{1})\otimes \overline{T}(X_{2})
\rightarrow \overline{T}(X_{1}\otimes X_{2})$ used in the description
of the product coalgebra is then the composite:
$$\xymatrix{
\varphi = \Big(FU(X_{1}) \otimes FU(X_{2})\ar[r]^-{\xi}_-{\cong} &
   F(U(X_{1})\times U(X_{2}))\ar[r]^-{T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}})} & FU(X_{1}\otimes X_{2})\Big)
}$$

\noindent where we consider the $X_i$ as algebras.

In order to see that $d$ is a map in $\textsl{CoAlg}\xspace(\overline{T})$ we
need to prove:
$$(b\times b) \mathrel{\circ} d = T(d) \mathrel{\circ} b.$$

\noindent We proceed in two steps.
$$\begin{array}{rcl}
(b\times b) \mathrel{\circ} d
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (b\otimes b) \mathrel{\circ}
   (a\otimes a) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   (T(b)\otimes T(b)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(b\times b) \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(\eta\times \eta) \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (\mu\otimes \mu) \mathrel{\circ}
   (T(\eta)\otimes T(\eta)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} T(d) \mathrel{\circ} b.
\end{array}$$

\noindent Similarly,
$$\begin{array}{rcl}
T(d) \mathrel{\circ} b
& = &
T(a\otimes a) \mathrel{\circ} T(\xi^{-1}) \mathrel{\circ} T^{2}(d) \mathrel{\circ} T(b) \mathrel{\circ} b \\
& = &
T(a\otimes a) \mathrel{\circ} T(\xi^{-1}) \mathrel{\circ} T^{2}(d) \mathrel{\circ} T(\eta) \mathrel{\circ} b \\
& = &
T(a\otimes a) \mathrel{\circ} T(\sigma) \mathrel{\circ} T(\eta) \mathrel{\circ} T(d) \mathrel{\circ} b \\
& & \qquad \mbox{with } \sigma = \xi^{-1} = t \mathrel{\circ} T(\eta\times\eta)
   \mbox{ as described above} \\
& = &
T(a\otimes a) \mathrel{\circ} T(t) \mathrel{\circ} T^{2}(\eta\times\eta) \mathrel{\circ} T(\eta) \mathrel{\circ}
   T(d) \mathrel{\circ} b \\
& = &
T(a\otimes a) \mathrel{\circ} T(t) \mathrel{\circ} T(\eta) \mathrel{\circ} T(\eta\times\eta) \mathrel{\circ}
   T(d) \mathrel{\circ} b \\
& = &
T(a\otimes a) \mathrel{\circ} T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} T(\eta\times\eta) \mathrel{\circ}
   T(d) \mathrel{\circ} b \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} T(a\times a) \mathrel{\circ} T(\eta\times\eta) \mathrel{\circ}
   T(d) \mathrel{\circ} b \\
& & \qquad\mbox{because $a$ is a homomorphism of algebras} \\
& = &
T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} T(d) \mathrel{\circ} b.
\end{array}$$

We can now prove the familiar tuple equations:
$$\begin{array}{rcl}
\pi_{1} \mathrel{\circ} \tuple{f_{1}, f_{2}}
& = &
\rho \mathrel{\circ} (\idmap\otimes u_{2}) \mathrel{\circ} (f_{1}\otimes f_{2}) \mathrel{\circ} d \\
& = &
\rho \mathrel{\circ} (f_{1}\otimes\idmap) \mathrel{\circ} (\idmap\otimes u) \mathrel{\circ} d \\
& = &
f_{1} \mathrel{\circ} \rho \mathrel{\circ} \rho^{-1} \\
& = &
f_{1} \\
\tuple{f_{1} \mathrel{\circ} g, f_{2} \mathrel{\circ} g}
& = &
((f_{1} \mathrel{\circ} g) \otimes (f_{2} \mathrel{\circ} g)) \mathrel{\circ} c \\
& = &
(f_{1}\otimes f_{2}) \mathrel{\circ} (g\otimes g) \mathrel{\circ} c \\
& = &
(f_{1}\otimes f_{2}) \mathrel{\circ} b \mathrel{\circ} g \\
& & \qquad \mbox{since $g$ is a map of coalgebras, and thus of comonoids} \\
& = &
\tuple{f_{1}, f_{2}} \mathrel{\circ} g.
\end{array}$$

The final equation requires more work:
$$\begin{array}{rcl}
\tuple{\pi_{1}, \pi_{2}}
& = &
(\pi_{1}\otimes\pi_{2}) \mathrel{\circ} d_{b_{1}\times b_{2}} \\
& = &
(\rho\otimes\lambda) \mathrel{\circ}
   ((\idmap\otimes u_{2}) \otimes (u_{1} \otimes \idmap)) \mathrel{\circ} \\
& & \qquad
   ((a_{1}\boxtimes a_{2}) \otimes (a_{1} \boxtimes a_{2})) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} (b_{1}\times b_{2}) \\
& = &
(\rho\otimes\lambda) \mathrel{\circ}
   ((a_{1}\boxtimes F(1)) \otimes (F(1) \boxtimes a_{2})) \mathrel{\circ} \\
& & \qquad
   (T(\idmap\otimes u_{2}) \otimes T(u_{1} \otimes \idmap)) \mathrel{\circ}
   \xi^{-1} \mathrel{\circ} T(\Delta) \mathrel{\circ} \varphi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} (T(\rho)\otimes T(\lambda)) \mathrel{\circ} \xi^{-1} \mathrel{\circ} \\
& & \qquad
   T((\idmap\otimes u_{2}) \times (u_{1} \otimes \idmap)) \mathrel{\circ}
   T(\Delta) \mathrel{\circ} \varphi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T((b_{1}\otimes b_{2}) \times (b_{1}\otimes b_{2})) \mathrel{\circ}
   T(\Delta) \mathrel{\circ} \varphi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T(\Delta) \mathrel{\circ} T(b_{1}\otimes b_{2}) \mathrel{\circ}
   \varphi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T(\Delta) \mathrel{\circ} \varphi \mathrel{\circ} (T(b_{1}) \otimes T(b_{2})) \mathrel{\circ}
   (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T(\Delta) \mathrel{\circ} \varphi \mathrel{\circ} (T(\eta) \otimes T(\eta)) \mathrel{\circ}
   (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T(\Delta) \mathrel{\circ} T(\eta\otimes\eta) \mathrel{\circ}
   \varphi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((a_{1}\otimes T(!)) \times (T(!) \otimes a_{2})) \mathrel{\circ} \\
& & \qquad
   T((\eta\otimes\eta) \times (\eta\otimes\eta)) \mathrel{\circ}
   T(\Delta) \mathrel{\circ} T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T((\idmap\otimes \eta) \times (\eta \otimes \idmap)) \mathrel{\circ} \\
& & \qquad
   T((\idmap\otimes\,!) \times (!\otimes\idmap)) \mathrel{\circ}
   T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}\times\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ} T(\Delta) \mathrel{\circ} \xi \mathrel{\circ}
   (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} T(\rho\times \lambda) \mathrel{\circ}
   T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}\times\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}}) \mathrel{\circ}
   T((\idmap\times \eta) \times (\eta \times \idmap)) \mathrel{\circ} \\
& & \qquad
   T((\idmap\times\,!) \times (!\times\idmap)) \mathrel{\circ}
   T(\Delta) \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ}
   T(\rho^{\times}\times \lambda^{\times}) \mathrel{\circ} \\
& & \qquad
   T((\idmap\times\,!) \times (!\times\idmap)) \mathrel{\circ}
   T(\Delta) \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& & \qquad\qquad \mbox{where }
   \rho^{\times} \colon A\times 1 \congrightarrow A,
   \mbox{see the `auxproof' of Theorem~\ref{MonadAlgStructThm}} \\
& = &
(a_{1}\otimes a_{2}) \mathrel{\circ} \xi^{-1} \mathrel{\circ} \xi \mathrel{\circ} (b_{1}\otimes b_{2}) \\
& = &
\idmap.
\end{array}$$

The restriction of the free functor $F\colon \cat{A} \rightarrow \textsl{Alg}\xspace(T)$
to $F\colon \cat{A} \rightarrow \textsl{CoAlg}\xspace(\overline{T})$, as in
Lemma~\ref{FreeAlgCoalgLem}, preserves finite products, since it
may be described as:
$$\xymatrix{
F(A) = \Big(\mu_{A}\ar[rr]^-{\delta_{\mu_A} = T(\eta_{A})} & & \mu_{TA}\Big)
}$$

\noindent so that $F(1)$ is the final object $1 = \delta_{\mu_1}$ as
described in the proof of~\ref{CoalgComonoidCor}. For binary
products, consider the following diagram in $\cat{A}$, forming
an isomorphism between coalgebras.
$$\hspace*{4em}\xymatrix@R-1pc@C-1pc{
\llap{$F(A\times B) = \Big($}T(A\times B)\ar[rrrr]^-{T(\eta_{A\times B})}
      \ar[drrr]^{T(\eta_{A}\times \eta_{B})}
   & & & & T^{2}(A\times B)\,\Big) \\
\llap{$F(A)\times F(B) = \Big($}T(A)\otimes T(B)\ar[u]^{\xi}_{\cong}
   \ar[rr]_-{T(\eta_{A})\otimes T(\eta_{B})} & &
   T^{2}(A)\otimes T^{2}(B)\ar[r]_-{\xi} &
   T(TA\times TB)\ar[r]_-{T(\mathrel{\raisebox{.05pc}{$\scriptstyle \otimes$}})}\ar[ur]^{T(\ensuremath{\mathsf{dst}})} &
   T(TA\otimes TB)\ar[u]_{T(\xi)}^{\cong}\,\Big)
}$$

\noindent The triangle on the right commutes by definition of
$\xi$, see the `auxproof' of Theorem~\ref{MonadAlgStructThm}.
Moreover, this isomorphism $\xi$ commutes with the projections:
$$\xymatrix{
T(A\times B)\ar[r]_-{T(\idmap\times\,!)}\ar @/^4ex/[rr]^-{T(\pi)} &
   T(A\times 1)\ar[r]_-{T(\rho)} & T(A)\ar@{=}[d] \\
T(A)\otimes T(B)\ar[u]^{\xi}_{\cong}\ar[r]^-{\idmap\otimes T(!)}
      \ar @/_4ex/[rr]_-{\pi} &
   T(A)\otimes T(1)\ar[u]^{\xi}_{\cong}\ar[r]^-{\rho} & T(A)
}$$
}

\section{Conclusions}

This paper elaborates the novel view that coalgebras-on-algebras are
bases, in a very general sense. This applies to coalgebras of the
comonad that is canonically induced on a category of algebras of a
monad. Various set-theoretic and order-theoretic examples support this
view. It remains to be investigated to what extent this view also
applies in program semantics, beyond the example of the exception
monad transformer. Also, the connection between bases and copying,
that is so important in quantum mechanics, exists in the current
abstract setting.

\subsection*{Acknoledgements} Thanks are due to Paul Blain Levy, Jorik
Mandemaker, and Paul Taylor, for helpful information and discussions
about the earlier version~\cite{Jacobs11d} of this paper.

\bibliographystyle{plain}