Note that per definition of $\widehat{\mathcal V}$, this set is always downwards-closed for $k\geq1$, and due to the $d_0$ codomain being the final object, it is also downwards-closed for $k=0$. We can now prove that $R_k=M^k$ for all $k$, proving the first claim, that two states can only get separated in both algorithms at the same time. We prove this via induction.

* Let $k=0$. Per definition, $R_0(x,y)=\Phi$ for all $x,y\in X$ and due to $d_0$ being the unique arrow into the final object, is must also hold that $M_0(x,y)=\Phi$ for all $x,y\in X$.

* Assume we have shown the claim for all $k'\leq k$.

* We will now show that the claim also holds for $k+1$. For this we show mutual inclusion.

* Let $\phi\in R_{k+1}(x,y)$ for any $\phi\in\Phi$, $x,y\in X$. Then $R_k(x,y)\ni\phi$ and – by definition of $F_1$ –  for all $a\in A$, $\phi'\leq\phi$, $x'\in\alpha(x)(a)(\phi')$ exists $y'\in\alpha(y)(a)(\phi')$ such that $R(x',y')\ni\phi'$ and – by definition of $F_2$ – vice versa. The induction allows us to find  $M^k(x,y)\ni\phi$ and for all $a\in A$, $\phi'\leq\phi$, $x'\in\alpha(x)(a)(\phi')$ there exists a $y'\in\alpha(y)(a)(\phi')$ such that $d_k(x')(\phi')=d_k(y')(\phi')$ (and vice versa). Therefore we can compute:
\begin{equation*}\begin{aligned}
&d_{k+1}(x)(\phi)(a)=\widehat{\mathcal V}d_k\circ\alpha(x)(\phi)(a)=\{(d_k(x')(\phi'),\phi')\mid\phi'\leq\phi,x'\in\alpha(x)(\phi')(a)\}\\
=&\{(d_k(y')(\phi'),\phi')\mid\phi'\leq\phi,y'\in\alpha(y)(\phi')(a)\}=\widehat{\mathcal V}d_k\circ\alpha(y)(\phi)(a)=d_{k+1}(y)(\phi)(a)
\end{aligned}\end{equation*}

Thus, $M^{k+1}(x,y)\ni\phi$.

* Let $M^{k+1}(x,y)\ni\phi$, i.e. $d_{k+1}(x)(\phi')(a)=d_{k+1}(y)(\phi')(a)$ for all $a\in A$, $\phi'\leq\phi$. Thus, by definition of $d_{k+1}$,

Therefore for all $\phi'\leq\phi$, $a\in A$, $x'\in\alpha(x)(\phi')(a)$, there must exist a $y'\in\alpha(y)(\phi')(a)$ such that $d_k(x')(\phi')=d_k(y')(\phi')$ and vice versa. Using the induction hypothesis we can therefore find, that $\phi'\leq\phi$, $a\in A$, $x'\in\alpha(x)(\phi')(a)$, there must exist a $y'\in\alpha(y)(\phi')(a)$ such that $\phi'\in R_k(x',y')$, proving $\phi\in F_1(R_k)(x,y)$ and vice versa, proving $\phi\in F_2(R_k)(x,y)$. Thus, $\phi\in R_{k+1}(x,y)$.

So we have seen that both algorithms separate pairs of states
in the same iteration. However, it still has to be shown that when no pairs of states are separated anymore, Algorithm <ref> terminates. Per definition, Algorithm <ref> terminates at that point, as well, so Algorithm <ref> can mimic Algorithm <ref>. So, let $d_n$ be such that $M_{n-1}=M_n$, and thus $R_{n-1}=R_n$, i.e. Algorithm <ref> has terminated. Further, let $x,y$ be given, such that $d_n(x)(\phi)\leq d_n(y)(\phi)$, i.e. for all $a\in A$, $d_n(x)(\phi)(a)\subseteq d_n(y)(\phi)(a)$. then
$$d_{n+1}(<x)(\phi)(a)=\widehat{\mathcal V}d_n\circ\alpha(x)(\phi)(a)=\{(d_n(x')(\phi'),\phi')\mid(x',\phi')\in\alpha(x)(\phi)\wedge\phi'\leq\phi\}$$
and analogously
We know that $d_n(x)(\phi)(a)\subseteq d_n(y)(\phi)(a)$, therefore, for $(x',\phi')\in\alpha(x)(\phi)$ there must exist a $(y',\phi')\in\alpha(y)(\phi)$ such that $d_{n-1}(x')(\phi')=d_{n-1}(y')(\phi')$. Since $M_{n-1}=M_n$, it must then also hold that $d_n(x')(\phi')=d_n(y')(\phi')$. Thus we can conclude $d_{n+1}(y)(\phi)(a)\supseteq d_{n+1}(x)(\phi)(a)$. Thus, Algorithm <ref> terminates in step $n$ as well.

Remove appendices from here onwards.

§ THE OLD SECTIONS ON THE LATTICE MONAD AND ITS EQUIVALENCE

Let $\lattice$ be a complete lattice satisfying the join-infinite distributive law:

\begin{equation}\label{eq:jid:old}
\ell \sqcap \bigsqcup L = \bigsqcup \{\ell \sqcap \ell' \mid \ell'\in L\},\quad (\text{for any}\ L\subseteq \lattice). \tag{$\mathsf{JID}$}
\end{equation}

For an ordered set $(X,\leq_X)$, let
$T(X,\leq_X)=(TX,\leq_{TX})$, where $TX=(X\rightarrow\mathbb L)^*$ is the set of all those functions $b\colon X\rightarrow\mathbb L$ satisfying the following restrictions:

*  $\bigsqcup_{x\in X}b(x)=\top$

*  For any $x,x'\in X$, we have
$b(x)\sqcap b(x')=
\bigsqcup\{b(y)\mid y\leq x,y\leq x'\}$.

*  For any join-irreducible element $\ell\in\mathcal
J(\lattice)$, the minimum of $\{x \mid \ell \le_\L b(x)\}$ exists,

\[
\exists_{x\in X}\ \ell\leq_\lattice b(x)\land \forall_{x'\in X}\
\big(\ell\leq_\lattice b(x') \implies x \leq_X
\]

Furthermore, for any two functions

$b, c\in (X\rightarrow\mathbb L)^*$ we let

\[b\leq_{TX}c\iff \forall_{x\in X}\ b(x)\geq_\lattice

It should be noted that Conditions <ref> and
<ref> in the above definition are redundant in the case
of finite distributive lattices in the following sense. Given a finite distributive lattice $\lattice$, an order preserving function $b\colon X\to\lattice$ satisfying Condition <ref> also satisfies Condition <ref>. Moreover, Condition <ref> and order preservation imply Condition <ref> in case of finite lattices.

For (<ref>), we note $\top=\bigsqcup_{\ell\in\mathcal J(\lattice)}\ell \leq_{\lattice} \bigsqcup_{\ell\leq b(x_\ell)} b(x_\ell) \leq_{\lattice} \bigsqcup_{x\in X} b(x)$. Here, $x_\ell=\smin \{x \mid \ell \leq_\lattice b(x)\}$ whose existence is guaranteed by Condition <ref>.

For (<ref>), we first note that the inequality $\bigsqcup_{y\leq_X x,y\leq_X x'} b(y) \leq_\lattice b(x) \sqcap b(x')$ (for any $x,x'\in X$) is equivalent to demanding that the function $b$ is order preserving. It is obvious that Condition <ref> implies $b$ is order preserving, simply let $x=x'$. On the other hand, if $b$ is order preserving, then from $y\leq x$ and $y\leq x'$ it follows that $b(y)\leq b(x)$ and $b(y)\leq b(x')$. Therefore, $b(x)\sqcap b(x')=\bigsqcup\{\ell\mid \ell\leq b(x)\wedge \ell\leq b(x')\}\geq_\lattice\bigsqcup\{b(y)\mid y\leq x\wedge y\leq x'\}.$

On the other hand, the inequality $\bigsqcup_{y\leq_X x,y\leq_X x'} b(y)\geq_\lattice b(x)\sqcap b(x')$ follows from Condition <ref> in the finite case because then
$$b(x)\sqcap b(x')=\bigsqcup\{\ell\in\mathcal J(\lattice)\mid\ell\leq b(x)\wedge \ell\leq b(x')\}\leq_\lattice\bigsqcup\{b(x_\ell)\mid x_\ell\leq x\wedge x_\ell\leq x'\}.$$

Lastly, Condition <ref> is required to rule out the cases when $X$ has an infinite descending chain $x_1\geq x_2\geq x_3 \cdots$ such that $\ell\leq_{\lattice} b(x_i)$ (for all $x_i\in X$). This is in-turn necessary to construct a corresponding function $C_b\in X^{\mathcal J(\lattice)}$ for a given $b\in TX$ such that $C_b(\ell) = \smin \{x \mid \ell \leq_\lattice b(x)\}$, (for every $\ell\in\mathcal J(\lattice)$).

Next we prove that $T$ is well-defined. Henceforth, we omit the index from the ordering relation, whenever it is clear from the context.

Every function in $(X \to \lattice)^*$ is order preserving.

Let $x \leq x'$, for some $x,x'\in X$. Then, by Condition  <ref>

\[
b(x)\sqcap b(x')\overset{\eqref{def:T-funk-2}}{=} \bigsqcup_{\substack{x''\leq x,\\ x''\leq
x'}} b(x'')
\overset{x\le x'}{=}\bigsqcup_{x''\leq
x}b(x'')\overset{\eqref{def:T-funk-2}}{=} b(x) \sqcap b(x) =b(x).
\]

Thus, $b(x)=b(x) \sqcap b(x')$, i.e., $b(x) \leq b(x')$.

If $f\colon X \to Y$ is order preserving and $b\in TX$ then $Tf(b)\in T(Y)$.

We need to show that $Tf(b)$ satisfies the three conditions of Definition <ref>. For Condition <ref>, we find $\bigsqcup_{y\in Y}Tf(b)(y)=\bigsqcup_{y\in Y}\bigsqcup_{f(x)\leq y}b(x)=\bigsqcup_{x\in X}b(x)=\top$.

For Condition <ref>, let $y,y'\in Y$. We need to show that $Tf(b)(y)\sqcap Tf(b)(y')=\bigsqcup_{\bar y\leq y\land\bar y\leq y'} Tf(b)(\bar y)$. By expanding the right hand side, we get

\[
\bigsqcup_{\bar y \leq y \land \bar y\leq y'}Tf(b)(\bar y)=\bigsqcup_{\bar y\leq y\land \bar y\leq y'}\bigsqcup_{f(x)\leq \bar y}b(x)=\bigsqcup_{f(x) \leq y\land f(x) \leq y'} b(x).
\]

For Condition <ref>, let $\ell\in\mathcal J(\lattice)$. Then, there is a minimal element $x_0$ satisfying $\ell \leq b(x_0)$. Clearly, $\ell \leq b(x_0) \leq \bigsqcup_{f(x)\leq f(x_0)} b(x) = Tf(b)(f(x_0))$. Now let $\ell \leq Tf(b)(y)$. Then, $\ell \leq \bigsqcup_{f(x)\leq y} b(x)$. I.e., $f(x)\leq y$ and $\ell \leq b(x)$, for some $x\in X$. But by Condition <ref>, we get $x_0\leq x$. And by order preservation of $f$ we get $f(x_0)\leq f(x) \leq y$; thus, $Tf(b)(f(x_0))\leq Tf(b)(y)$.

If $f\colon (X,\leq_X)\rightarrow (Y,\leq_Y)$ is order preserving, then so is $Tf$.

Let $f\colon (X,\leq_X)\rightarrow (Y,\leq_Y)$ be an order preserving function. Then, we want to prove that $Tf\colon T(X,\leq_X)\rightarrow T(Y,\leq_Y)$ is also order preserving. Let $b\leq_{TX}b'$, for some $b,b'\in (X \to \lattice)^*$. Then, we have $b'(x) \leq_\lattice b(x)$, for any $x\in X$. Thus, we have

\[Tf(b')(y)=\bigsqcup_{f(x)\leq_Y y}b'(x) \leq_{\lattice} \bigsqcup_{f(x)\leq_Y y}b(x) = Tf(b)(y).\]

Hence, $Tf$ is order preserving.

Now we prove that $T$ is actually a functor.

The mapping $T$ as in Definition <ref> is an endofunctor.

We start by showing the preservation of identities:

\[(T\mathsf{id})(b)(y)=\bigsqcup_{\mathsf{id}(x)\leq y}b(x)=\bigsqcup_{x\leq y}b(x)=\bigsqcup_{x=y}b(x)=b(y)=\mathsf{id}_T(b)(y).\]

To show that $T$ respects concatenation of arrows, we derive:

\begin{align*}
(Tf\circ Tg)(b)(z)=&\ Tf(Tg(b))(z)=\bigsqcup_{f(y)\leq z}Tg(b)(y)=\bigsqcup_{f(y)\leq z}\bigsqcup_{g(x)\leq y}b(x),\\
T(f\circ g)(b)(z)=&\ \bigsqcup_{(f\circ g)(x)\leq z}b(x).
\end{align*}

Now we will prove that the sets over which the supremum is taken are identical, making the suprema themselves identical.

* If $f(g(x))\leq z$, then let $y:=g(x)$, then automatically $y\geq g(x)$ and additionally $f(y)\leq z$.

* If $y\geq g(x)$ and $z\geq f(y)$ then $z\geq f(y)\geq f(g(x))$ due to monotonicity of $f$.

Next, we define a unit and a multiplication associated with our functor $T$, which in turn give rise to the lattice monad.

Define two families of maps $\eta_X\colon X \to TX$ and $\mu_X\colon TTX \to TX$:

\begin{align*}
\eta_X(x)(x')=&\
\begin{cases}
\top&\text{if\ }x\leq x'\\
\bot&\text{otherwise}
\end{cases}\enspace,\\
\mu_X(\widehat B)(x)=&\
\bigsqcup_{b\in(X\rightarrow\mathbb L)^*}(\widehat B(b)\sqcap b(x)),
\qquad \text{where}\ \widehat B\in((X\rightarrow\mathbb L)^*\rightarrow\mathbb L)^*.
\end{align*}

In the remainder, we show that the families of functions $\eta$ and
$\mu$ are well-defined resulting in natural transformations between
the functors $\text{Id} \Rightarrow T$ and $TT\Rightarrow T$,
respectively. The corresponding lemmas are stated below and the proofs
can be found in Appendix <ref>.

Now that $\eta$ and $\mu$ are well-defined natural transformations, we
investigate whether the so-called unit and associative
law of a monad hold or not, again the proofs are in
Appendix <ref>.

Next we state the main result of this section.
The tuple $(T,\eta,\mu)$ is a monad on $\pos$.

§.§ Equivalence of Lattice Monad and Reader Monad

In this section, using the famous Birkhoff's representation theorem,
we show that the Kleisli categories of the lattice monad and the
reader monad are actually

Throughout this section, we fix $(\Phi,\leq_\Phi)$ as a finite partially ordered set and
$\lattice$ is the set of all downward closed subsets of $\Phi$. Recall
that every downward-closed subset of $\Phi$ can be represented by a
principal ideal of $\lattice$.  As a result, in the sequel, we do not
distinguish between the elements of $\lattice$ and $\Phi$.

We define a natural transformation $\alpha\colon T\Rightarrow {\_}^\Phi$ and
prove that $\alpha$ is a natural isomorphism and monad morphism. Hence, the
monad's Kleisli categories are isomorphic as well.

Define two families of arrows $\alpha_X\colon TX \to (X,\leq_X)^{(\Phi,\leq_\Phi)}$ and $\inv{\alpha_X}\colon (X,\leq_X)^{(\Phi,\leq_\Phi)} \to TX$ (for each ordered set $X$) in the following way:

\begin{align*}
\alpha_X(b)(\phi) &= \smin \{x\mid b(x)\geq \phi\} \quad (\text{for every $b\in TX$ and $\phi\in \Phi$}),\\
\inv{\alpha_X}(C)(x) &= \bigsqcup\{\phi\mid C(\phi)\leq_X x\}\quad
(\text{for every $C\in
(X,\leq_X)^{(\Phi,\leq_\Phi)}$ and $x\in
X$}).%\todo{B: Why do you use a capital $C$ here?}
\end{align*}

For an object in $\pos$, the induced functions $\alpha$ and $\inv{\alpha}$ are arrows in $\pos$.

Let $(X,\leq_X)$ be an ordered set. To show that $\alpha_X$ is order preserving, let $b_2\leq_{TX} b_1$, for some $b_1,b_2\in TX$. I.e., $b_1(x)\leq b_2(x)$ for all $x\in X$ (remember the reversal of orders in the lattice monad $T$).
Since $b_1(x)\leq b_2(x)$ for all $x\in X$, it must hold

\begin{equation*}\begin{aligned}
&b_1(x)\geq\phi\implies b_2(x)\geq\phi\\
\implies&\{x\mid b_1(x)\geq\phi\}\subseteq\{x\mid b_2(x)\geq\phi\}\\
\implies&\mathsf{min}\{x\mid b_1(x)\geq\phi\}\geq\mathsf{min}\{x\mid b_2(x)\geq\phi\} \implies
\alpha_X(b_1)(\phi)\geq\alpha_X(b_2)(\phi).
\end{aligned}\end{equation*}

And to show that $\inv{\alpha_X}$ is order preserving, let $C_1\leq C_2$. Now if $C_1(\phi)\leq_X C_2(\phi)$ (which is always true), then $C_2(\phi)\leq_X x$ implies $C_1(\phi)\leq x$, thus, $\alpha^{-1}_X(C_1)(x)\geq\alpha_X^{-1}(C_2)(x)$ for all $x$ and, due to the reversal of the order in $T$, $\alpha^{-1}_X(C_1)\leq\alpha_X^{-1}(C_2)$.

Next, we show that the functions $\alpha_X$ and $\inv{\alpha_X}$ (for an ordered set $(X,\leq_X)$) are well defined. The next lemma proves this fact.

Let $(X,\leq_X)$ be an ordered set.

* If $b\in TX$, then $\alpha_X(b)\in (X,\leq_X)^{(\Phi,\leq_\Phi)}$, i.e., $\alpha_X(b)$ is order preserving.

* If $C\in (X,\leq_X)^{(\Phi,\leq_\Phi)}$, then $\inv{\alpha_X}(C)\in TX$.

For (1), let $\phi\leq_\Phi \phi'$. Then, we need to show that $\alpha_X(b)(\phi) \leq_X \alpha_X(b)(\phi')$, which follows directly from the fact that $\{x\mid \phi'\leq_\mathbb L b(x)\}\subseteq\{x\mid \phi\leq_\mathbb L b(x)\}$ holds.

For (2), let $C\in (X,\leq_X)^{(\Phi,\leq_\Phi)}$. Then, we distinguish the following cases:

Condition <ref> Using the fact that $C\in (X,\leq_X)^{(\Phi,\leq_\Phi)}$ is a total function, we obtain
$$\bigsqcup_{x\in X} \inv{\alpha_X}(C)(x) = \bigsqcup_{x\in X} \bigsqcup_{C(\phi)\leq_X x} \phi = \bigsqcup \Phi =\top.$$

Condtion <ref> Let $x,x'\in X$. Then, using distributivity we find

\[\inv{\alpha_X}(C)(x) \sqcap \inv{\alpha_X}(C)(x')
\bigsqcup_{C(\phi)\leq_X x} \phi \sqcap \bigsqcup_{C(\phi')\leq_X x'} \phi'
\bigsqcup_{C(\phi)\leq_X x,C(\phi')\leq_X x'} \phi \sqcap \phi'.
\]

\[\bigsqcup_{\bar x\leq_X x,\bar x\leq_X x'} \inv{\alpha_X}(C)(\bar x)
\bigsqcup_{\bar x\leq_X x,\bar x\leq_X x'} \bigsqcup_{C(\phi)\leq \bar x} \phi
=\bigsqcup_{C(\phi)\leq_X x,C(\phi)\leq_X x'} \phi.\]

Next, we show that $\{\phi\mid C(\phi)\leq_X x, C(\phi)\leq_X x'\}=\{\phi\sqcap\phi'\mid C(\phi)\leq_X x, C(\phi')\leq_X x'\}$ to complete the proof for this case. The direction `$\subseteq$' is obvious because $\phi =\phi \sqcap \phi$. For the other direction, let $C(\phi)\leq_X x$ and $C(\phi')\leq_X x'$. Then, using order preservation of $C$ we find $C(\phi \sqcap \phi') \leq C(\phi) \leq_X x$. Likewise, $C(\phi \sqcap \phi') \leq_X x'$.

Condition <ref> Let $\phi$ be a join irreducible element and let $x=C(\phi)$. Then, we find that $\phi \leq \bigsqcup_{C(\phi')\leq C(\phi)} \phi= \inv{\alpha_X}(C)(x)$. Now suppose $\phi \leq \inv{\alpha_X}(C)(x')$, for some $x'\in X$. Then, $\phi\leq \bigsqcup_{C(\phi')\leq_X x'} \phi'$. Since $\phi$ is join-irreducible, we get $C(\phi)\leq_X x'$ as required.

To show that $\alpha$ and $\alpha^{-1}$ are isomorphisms between the two Kleisli categories, we will proceed to show that they are each other's inverses.
The transformations $\alpha$ and $\alpha^{-1}$ are each other's inverses.

Let $(X,\leq_X)$  be an ordered set. Then we distinguish the following cases.

* To show $\inv{\alpha_X}\circ\alpha_X(b)=b$, for
$b\in TX$. Expanding $\inv{\alpha_X}\circ\alpha_X(b)$ we get

\inv{\alpha_X}(\alpha_X(b))(x)=\bigsqcup\{\phi \mid \alpha_X(b)(\phi)\leq_X x\}
\bigsqcup\{\phi\mid\mathsf{min}\{y\mid \phi\leq b(y)\}\leq x\} .

Now, if $\phi\leq b(x)$, then
$x\geq \mathsf{min}\{y\mid \phi\leq b(y)\}$ and thus
$\phi\leq \inv{\alpha_X}(\alpha_X(b))(x)$. If, on the other hand,
$\phi\leq \inv{\alpha_X}(\alpha_X(b))(x)$ holds, then there is a $y\in X$ such that $\phi\leq b(y)$ and $y\leq x$. Since $b$ is order preserving, it follows that $\phi\in b(x)$.

* To show $\alpha_X\circ\inv{\alpha_X}(C)=C$, for $C\in(X,\leq_X)^{(\Phi,\leq_\Phi)}$. Expanding $\alpha_X\circ\inv{\alpha_X}(C)$ we get

\phi\}=\mathsf{min}\{x\mid\bigsqcup\{\phi'\mid C(\phi')\leq
x\}\geq \phi\}.$$

C(\phi)\leq x
\Rightarrow
\bigsqcup\{\phi'\mid C(\phi')\leq x\}\geq \phi
\Rightarrow
x\geq\mathsf{min}\{x\mid\bigsqcup\{\phi'\mid C(\phi')\leq x\}\geq\phi\}

If, on the other hand, $x\geq\alpha_X(\inv{\alpha_X}(C))(\phi)$, i.e.
$x\geq \mathsf{min}\{x\mid\bigsqcup\{\phi'\mid C(\phi')\leq
x\}\geq \phi\}$,
$y:=\mathsf{min}\{x\mid\bigsqcup\{\phi'\mid C(\phi')\leq x\}\geq
\phi\}$.
Then, $\bigsqcup\{\phi'\mid C(\phi')\leq y\}\geq \phi$ holds. Since $\phi$ is a join-irreducible element, we find $\phi\leq \phi'$ and $C(\phi')\leq y$, for some $\phi'$. Lastly, order preservation of $C$ and transitivity of $\leq$ together yields $C(\phi)\leq x$.

Henceforth, throughout this section, for an order preserving function $f\colon (X,\leq_X) \to (Y,\leq_Y)$, we write $f^\Phi$ to denote the image of $f$ under the reader monad, i.e., $f^\Phi(C)=f\circ C$, for any $C\in (X,\leq_X)^{(\Phi,\leq_\Phi)}$.

The family $\alpha$ given in Definition <ref> is a natural transformation.

Given an order preserving function $f:(X,\leq_X)\rightarrow (Y,\leq_Y)$, we need to show $\alpha_Y(T(f)(b))(\phi)=f^\Phi(\alpha_X(b))(\phi)$, for any $b\in TX$ and $\phi\in \Phi$.

\begin{align*}f^\Phi(\alpha_X(b))(\phi)=f(\alpha_X(b))(\phi)=f(\mathsf{min}\{x\mid b(x)\geq \phi\})=\mathsf{min}\{f(x)\mid b(x)\geq \phi\}\end{align*}

In the last step we used monotonicity of $f$. On the other hand we have:

\begin{align*}\alpha_Y(T(f)(b))(\phi)=\mathsf{min}\{y\mid Tf(b)(y)\geq \phi\}=\mathsf{min}\{y\mid\bigsqcup\{b(z)\mid f(z)\leq y\}\geq \phi\}\end{align*}

We will now show that both the expressions are equal.

* Let $f(x)\in\{f(x)\mid b(x)\geq \phi\}$, i.e. $x$ be chosen such that $b(x)\geq \phi$. Then, $\bigsqcup\{b(z)\mid f(z)\leq f(x)\}\geq \phi$ and therefore $f(x)\in\{y\mid\bigsqcup\{b(z)\mid f(z)\leq y\}\geq \phi\}$. So, in particular, $f(x)\geq \mathsf{min}\{y\mid\bigsqcup\{b(z)\mid f(z)\leq y\}\geq \phi\}$.

* Let $y\in\{y'\mid\bigsqcup\{b(z)\mid f(z)\leq y'\}\geq \phi\}$. Since $\phi$ is join-irreducible, there must be a $z$ such that $f(z)\leq y$ and $b(z)\geq \phi$, i.e. $y\geq \mathsf{min}\{f(x)\mid b(x)\geq \phi\}$.

Now we want to show that $\alpha$ preserves the unit.

The natural transformation $\alpha$ is a monad morphism, that is,
$\alpha$ preserves the unit and the multiplication.

Diagramatically speaking,

\[
\begin{tikzcd}
\arrow{d}[swap]{\eta_X}
\arrow{dr}{\nu_X}
\\
\arrow{r}{\alpha_X}
\end{tikzcd}
\quad\text{ and }\quad
\begin{tikzcd}
\arrow{r}{(\alpha*\alpha)_X}
\arrow{d}[swap]{\mu_X}
\arrow{d}{\zeta_X}
\\
\arrow{r}{\alpha_X}
\end{tikzcd}
\]

commute, where $\alpha*\alpha$ is the Godement product $(\alpha*\alpha)_X =
\alpha_X^\Phi\cdot \alpha_{TX}$ (or equivalently $ = \alpha_{X^\Phi}\cdot
T\alpha_X$ by naturality).b: Why does this equality hold?

The unit is preserved because

\[
\alpha_X(\eta_X(x))(\phi)
=\mathsf{min}\{y\mid\eta_X(x)(y)\geq \phi\}
=\mathsf{min}\{y\mid x\leq y\}=\nu_X(x)(\phi).
\]

For the multiplication, see the appendixMaybe this lemma can be dropped
completely; if not, the lemma in the appendix can be simplified by dropping $g$

Since $\alpha$ also natural isomorphism, it proves $T \cong
\_^\Phi$. It is a standard exercise to see that there is a one-to-one
correspondence between monad morphisms and functors between their
Kleisli categoriesCite: Prop. 4.0.10 of An abstract view
of programming languages by Eugenio Moggi. So $\alpha$ induces
an isomorphism between categories
$\mathsf{Kl}(T)\xrightarrow{\cong} \mathsf{Kl}(\_^\Phi)$, defined as

\[
(f: X\to TY) \mapsto (\alpha_X\cdot f: X\to Y^\Phi).
\]

When proving the equivalence of the reader monad and the lattice
monad, the duality between complete finite distributive lattices and
partially ordered sets plays an important role, namely when defining
the isomorphisms $\alpha$ and $\alpha^{-1}$. Considering there is a
similar duality between complete distributive lattices (not
necessarily finite) and clopen downsets on Priestley spaces – i.e.
spaces of partially ordered sets with a topology that makes them
totally order disconnected – one might wonder why we restrict to
the finite variant.

To make a similar duality result work for the infinite case, we
would need to restrict the lattices with additional assumptions,
because not all bounded distributive lattices are isomorphic to a
lattice of downsets of a partial order. This holds if additionally
the JID and its dual hold and some notion of atomicity holds for the
irreducibles in the lattice [13].  This however
would make the definition of the lattice monad more complicated.

We first show that $\eta_X\in TX$, for any ordered set $X$. Condition <ref> follows directly $\bigsqcup_{x'\in X} \eta_X(x)(x')=\top$.
And for Condition <ref>, let $x',x''\in X$. Then we find

\[
\bigsqcup \{\eta_X(x)(\bar x)\mid \bar x \leq x' \land \bar x \leq x''\}=
\bigsqcup \{\top \mid x \leq \bar x \land \bar x \leq x' \land \bar x \leq x''\}=\eta_X(x)(x') \sqcap \eta_X(x)(x'').
\]

Lastly, for Condition <ref>, given a join-irreducible element $\ell\in\mathcal J(\lattice)$, we have $\ell\leq \top=\eta_X(x)(x)$. Moreover, if $\ell\leq \eta_X(x)(x')$, then clearly we have $x\leq x'$.

We also need to show that $\eta_X$ is an arrow in $\pos$. For that purpose let $x\leq x'$ and an arbitrary $\overline x\in X$ be given, then
$$\eta_X(x)(\overline x)=\begin{cases}\top&\text{if\ }x\leq\overline x\\\bot&\text{otherwise}\end{cases}\geq\begin{cases}\top&\text{if\ }x'\leq\overline x\\\bot&\text{otherwise}\end{cases}=\eta_X(x')(\overline x)$$

Due to the reversal of orders in $TX$, this actually means $\eta_X(x)\leq\eta_X(x')$, so $\eta_X$ is order preserving.

Next, it remains to verify that the function $\eta_X$ satisfies the naturality square. So let $f:(X,\leq_X)\rightarrow(Y,\leq_Y)$. Then, we find

\[Tf(\eta_X(x))(y)= \bigsqcup_{f(x') \leq_{Y} y} \eta_X(x)(x')= \bigsqcup_{f(x') \leq_{Y} y\land x\leq_X x'} \top= \bigsqcup_{f(x)\leq_Y y} \top = \eta_Y(f(x))(y).\]

First we show that for any $\widehat B\in((X\rightarrow\mathbb L)^*\rightarrow\mathbb L)^*$, we have $\mu_X(\widehat B)\in TX$. To see that Condition <ref>(<ref>) holds, we expand $\bigsqcup_{x\in X}\mu_X(\widehat B)(x)$ and derive:

\[ \bigsqcup_{x\in X}\bigsqcup_{b\in(X\rightarrow\mathbb L)^*}(\widehat B(b)\sqcap b(x)) = \bigsqcup_{b\in(X\rightarrow\mathbb L)^*}\bigsqcup_{x\in X}(\widehat B(b)\sqcap b(x)) =\bigsqcup_{b\in(X\rightarrow\mathbb L)^*}\widehat B(b)\sqcap(\bigsqcup_{x\in X} b(x)) = \top.\]

For Condition <ref>(<ref>), the direction $\bigsqcup_{\bar x\leq x\land \bar x\leq x'} \mu_X(\widehat B)(\bar x)\leq_\lattice \mu_X(\widehat B)(x)\sqcap \mu_X(\widehat B)(x')$ is straightforward because $\widehat B(b) \sqcap b(\bar x) \leq \widehat B(b) \sqcap b(x)$ whenever $\bar x\leq x$, for any $b\in TX$. For the other direction, we first note by applying JID law twice that
\mu_X(\widehat B)(x) \sqcap \mu_X(\widehat B)(x')
\bigsqcup_{b,b'} \bigl( \widehat B(b) \sqcap b(x) \sqcap \widehat B(b') \sqcap b'(x')\bigr).
It is sufficient to show that for any $b,b'\in TX$ we have
\widehat B(b) \sqcap b(x) \sqcap \widehat B(b') \sqcap b'(x')
\leq_\lattice
\bigsqcup_{\bar x \leq x \land \bar x\leq x'} \mu_X(\widehat B) (\bar x).
So, let $b,b'\in TX$. Then we derive

\begin{align*}
\widehat B(b) \sqcap \widehat B(b') \sqcap b(x) \sqcap b'(x')
& \stackrel{\eqref{def:T-funk-2}}{=}
\left(\bigsqcup_{\bar b\leq b\land\bar b\leq b'} \widehat B(\bar b)\right) \sqcap b(x) \sqcap b'(x') \qquad (\text{$\jid$ law}) \\
& =
\bigsqcup_{\bar b\leq b\land \bar b\leq b'} \left(\widehat B(\bar b) \sqcap b(x) \sqcap b'(x')\right) \qquad (\text{Def. of}\ \leq_{TX})\\
& \leq_\lattice
\bigsqcup_{\bar b\leq b\land \bar b\leq b'} \left(\widehat B(\bar b) \sqcap \bar b(x) \sqcap \bar b(x')\right) \qquad (\text{Def}.\ref{def:T-Funktor}\eqref{def:T-funk-2})\\
& =
\bigsqcup_{\bar b\leq b\land \bar b\leq b'} \left(\widehat B(\bar b) \sqcap \bigsqcup_{\bar x\leq x\land \bar x\leq x'} \bar b(\bar x)\right)  \qquad (\text{$\jid$ law}) \\
& =
\bigsqcup_{\bar b\leq b\land \bar b\leq b'} \bigsqcup_{\bar x\leq x\land \bar x\leq x'} \left(\widehat B(\bar b) \sqcap \bar b(\bar x)\right)\\
& =
\bigsqcup_{\bar x\leq x\land \bar x\leq x'} \bigsqcup_{\bar b\leq b\land \bar b\leq b'} \left(\widehat B(\bar b) \sqcap \bar b(\bar x)\right)\\
& \leq_\lattice
\bigsqcup_{\bar x\leq x\land \bar x\leq x'} \bigsqcup_{\bar b\in TX} \left(\widehat B(\bar b) \sqcap \bar b(\bar x)\right) =
\bigsqcup_{\bar x\leq x\land \bar x\leq x'}  \mu_X(\widehat B)(\bar x).
\end{align*}

Lastly for Condition <ref>(<ref>), let $\ell\in\mathbb L$ be a join-irreducible element. Since $\widehat B\in((X\rightarrow\mathbb L)^*\rightarrow\mathbb L)^*$, there is a minimal $b_0\in(X\rightarrow\mathbb L)^*$ such that $\ell \leq \widehat B(b_0)$. I.e., for any $b\in (X\rightarrow\mathbb L)^*$ with $\ell \leq \widehat B(b)$ we have $b(x)\leq b_0(x)$, for all $x\in X$.
Moreover, there is a minimal $x_0\in X$, such that $\ell \leq b_0(x_0)$, since $b_0\in (X\rightarrow\mathbb L)^*$. Then, we find $\ell\leq \widehat B(b_0) \sqcap b_0(x_0)$, i.e., $\ell \leq \mu_X(\widehat B)(x_0)$. Now let $x\in X$ such that $\ell\leq \mu_X(\widehat B)(x)$. Thus, it remains to show that $\mu_X(\widehat B)(x_0) \leq \mu_X(\widehat B)(x)$. To see this, we first observe that $\ell=\ell \sqcap \mu_X(\widehat B)(x) = \bigsqcup_{b} (\ell \sqcap \widehat B(b) \sqcap b(x))$. And since $\ell$ is join-irreducible we find $\ell \leq \widehat B(b) \sqcap b(x)$, for some $b\in (X\to \lattice)^*$. Clearly, $\ell\leq b(x) \leq b_0(x)$, (since $b_0\leq b$) and $\ell \leq \widehat B(b)$. Thus, by minimality of $x_0$, we find $x_0\leq x$; hence, $b(x_0) \leq b(x)$.

We further need to show that $\mu_X$ is an arrow in $\pos$. For that purpose let $\widehat B\leq\widehat B'$ and any $x\in X$ be given and compute

$$\mu_X(\widehat B)(x)=\bigsqcup_{b\in(X\rightarrow\mathbb L)^*}\widehat B(b)\sqcap b(x)\geq\bigsqcup_{b\in(X\rightarrow\mathbb L)^*}\widehat B'(b)\sqcap b(x)=\mu_X(\widehat B')(x)$$

because of the reversal of order: If $\widehat B\leq\widehat B'$, then $\widehat B(b)\geq\widehat B'(b)$ for all $b\in(X\rightarrow\mathbb L)^*$. Now, again because of the reversal of orders, it follows that $\mu_X(\widehat B)\leq\mu_X(\widehat B')$, so $\mu_X$ is order preserving.

Now it remains to show that the $\mu_X$ satisfies the naturality square. Let $\widehat B\in((X\rightarrow\mathbb L)^*\rightarrow\mathbb L)^*$ and $y\in Y$. Then, we find

\[
Tf(\mu_X(\widehat B))(y)=\bigsqcup\{\widehat B(b)\sqcap b(x)\mid fx \leq y \land b\in TX\}.\]

\begin{align*}
(\mu_Y\circ TTf(\widehat B))(y)
=&\ \bigsqcup \{TTf(\widehat B)(c) \sqcap c(y) \mid c\in TY\}\\
=&\ \bigsqcup \left\{ \left(\bigsqcup_{Tf(b)\leq c} \widehat B(b)\right) \sqcap c(y) \mid c\in TY\right\}  \quad (\text{$\jid$ law}) \\
=&\ \bigsqcup \{ \widehat B(b) \sqcap c(y) \mid c\in TY\land Tf(b)\leq c \}\\
=&\ \bigsqcup \{ \widehat B(b) \sqcap c(y) \mid TY \land \forall_{y'\in Y}\ c(y')\leq Tf(b)(y') \}.%\\
%=&\ \bigsqcup \{ \widehat B(b) \sqcap c(y) \mid c\in TY \land \forall_{y'\in Y}\ c(y')\leq \bigsqcup_{f(x)\leq y'} b(x) \}.
\end{align*}

Suppose there are $b\in TX,c\in TY$ such that $\forall_{y'}\ c(y')\leq Tf(b)(y')$. Thus, $c(y)\leq Tf(b)(y)=\bigsqcup_{f(x)\leq y} b(x)$. I.e., $\widehat B(b) \sqcap c(y) \leq \widehat B(b) \sqcap \bigsqcup_{f(x)\leq y} b(x)$. Thus,
$(\mu_Y\circ TTf(\widehat B))(y)\leq Tf(\mu_X(\widehat B))(y)$. The other direction is straightforward, take $c=Tf(b)$.

Let $x\in X$ and $\widehat C \in TTTX$. We first compute $\mu_X\circ \mu_{TX}$ (below $b\in TX,\widehat B\in TTX$):

\begin{align*}
\mu_X(\mu_{TX}(\widehat C))(x)
=&\ \bigsqcup_{b}(\mu_{TX}\bigl(\widehat C)(b)\sqcap b(x)\bigr) \\
=&\ \bigsqcup_{b}\Big(\bigsqcup_{\widehat B}\Big(\widehat C(\widehat B) \sqcap \widehat B(b)\Big) \sqcap b(x)\Big) && (\text{$\jid$ law}) \\
=&\ \bigsqcup_{b}\bigsqcup_{\widehat B} \left(\widehat C (\widehat B) \sqcap \widehat B(b) \sqcap b(x) \right)\\
=&\ \bigsqcup_{\widehat B} \bigsqcup_b \left(\widehat C (\widehat B) \sqcap \widehat B(b) \sqcap b(x) \right) && (\text{$\jid$ law}) \\
=&\ \bigsqcup_{\widehat B} \widehat C(\widehat B) \sqcap \bigsqcup_b \left(\widehat B(b) \sqcap b(x) \right)\\
=&\ \bigsqcup_{\widehat B} (\widehat C(\widehat B) \sqcap \mu_X(\widehat B)(x)).%\\
%	=&\ \bigsqcup\left\{\widehat C(\widehat B)\sqcap \mu_X(\widehat B)(x) \mid  \widehat B\in((X\rightarrow\mathbb L)^*\rightarrow\mathbb L)^*\right\}.
\end{align*}

Furthermore, we compute $\mu_X\circ T(\mu_X)$ as follows:

\begin{align*}
\mu_X(T(\mu_X)(\widehat C))(x)
=&\ \bigsqcup_b \Big(T(\mu_X(\widehat C))(b)\sqcap b(x)\Big)\\
\Big(
\Big(\bigsqcup_{\mu_X(\widehat B)\leq b} \widehat C(\widehat B)\Big)
\sqcap
b(x)\Big) && (\text{$\jid$ law}) \\
\bigsqcup_{\mu_X(\widehat B)\leq b} \Big(\widehat C(\widehat B)
\sqcap b(x)\Big).%\\
%    =&\bigsqcup
%        \left\{
%            \widehat C(\widehat B) \sqcap b(x)
%            \mid b\in (X \to \lattice)^*
%                \land \forall_{x'}\ b(x') \leq \mu_X(\widehat B)(x')
%        \right\}.
%    =&\bigsqcup
%        \left\{
%            \widehat C(\widehat B) \sqcap b(x)
%            \mid b\in (X \to \lattice)^*
%                \land \forall_{x'}\ b(x') \leq \bigsqcup_{b'\in (X \to \lattice)^*} \widehat B(b') \sqcap b'(x')
%        \right\}.
\end{align*}

Now, we observe that $\widehat C (\widehat B) \sqcap b(x) \leq \widehat C (\widehat B) \sqcap  \mu_X(\widehat B)(x)$, for any $b$ satisfying $b(x')\leq \mu_X(\widehat B)(x')$ (for any $x'\in X$). Thus, $\mu_X(T(\mu_X)(\widehat C))(x) \leq \mu_X(\mu_{TX}(\widehat C))(x)$. For the other direction, take $b=\mu_X(\widehat B)$; thus, $\mu_X(\mu_{TX}(\widehat C))(x)\leq \mu_X(T(\mu_X)(\widehat C))(x)$.

We first expand the left hand side

\begin{align*}
&\mu_X(\eta_{TX})(b)(y)=\bigsqcup\{\eta_{TX}(b)(d)\sqcap d(y)\mid d\in(X\rightarrow\mathbb L)^*\}\\
=&\bigsqcup\{d(y)\mid b\leq d\}=\bigsqcup\{d(y)\mid \forall x\in X: b(x)\geq d(x)\}=b(y).
\end{align*}

Furthermore, expanding the right hand side we get

\begin{align*}
&\mu_X(T\eta_X)(b)(y)=\bigsqcup\{T\eta_X(b)(d)\sqcap d(y)\mid d\in(X\rightarrow\mathbb L)^*\}\\
=&\bigsqcup\{b(x)\sqcap d(y)\mid d\in(X\rightarrow\mathbb L)^*, \eta_X(x)\leq d\}\\
=&\bigsqcup\{b(x)\sqcap d(y)\mid d\in(X\rightarrow\mathbb L)^*, \forall x'\in X: \eta_X(x)(x')\geq d(x')\}\\
=&\bigsqcup\{b(x)\mid x\leq y\}=b(y).
\end{align*}

Let $b\in T(Y)$, $\phi\in\Phi$. We compute:

\begin{align*}
&(\alpha_Z\circ\mu_Z\circ Tg)(b)(\phi)=\mathsf{min}\{z\mid(\mu_Z\circ Tg)(b)(z)\geq \phi\}\\
=\ &\mathsf{min}\{z\mid\bigsqcup\{Tg(b)(d)\sqcap d(z)\mid d\in(Z\rightarrow\mathbb L)^*\}\geq \phi\}\\
=\ &\mathsf{min}\{z\mid\bigsqcup\{b(y)\sqcap d(z)\mid d\in(Z\rightarrow\mathbb L)^*, g(y)\leq d\}\geq \phi\}.
\end{align*}

as well as

\begin{align*}
&(\zeta_Z\circ\alpha_Z^\Phi\circ g^\Phi\circ\alpha_Y)(b)(\phi)=(\alpha_Z^\Phi\circ g^\Phi\circ\alpha_Y)(b)(\phi)(\phi)\\
=\ &(\alpha_Z\circ g^\Phi\circ\alpha_Y)(b)(\phi)(\phi)=\mathsf{min}\{z\mid g^\Phi\circ\alpha_Y(b)(\phi)(z)\geq \phi\}\\
=\ &\mathsf{min}\{z\mid g(\alpha_Y(b)(\phi))(z)\geq \phi\}=\mathsf{min}\{z\mid g(\mathsf{min}\{y\mid \phi\leq b(y)\})(z)\geq \phi\}.
\end{align*}

It is sufficient to show that the following conditions are logically equivalent (for every $z\in Z$):

\[\phi \leq \bigsqcup_{g(y)\leq d,d\in TZ} (b(y) \sqcap d(z)) \iff
\phi \leq g(\smin\{y \mid \phi \leq b(y)\})(z).\]

$\Leftarrow$ Fix $\bar y = \smin \{y \mid \phi \leq b(y)\},d=g(\bar y)$. Thus, $\phi \leq b(\bar y) \sqcap d(z) \leq \bigsqcup_{g(y)\leq d,d\in TZ} (b(y) \sqcap d(z))$.
$\Rightarrow$ Assume $\phi \leq \bigsqcup_{g(y)\leq d,d\in TZ} (b(y) \sqcap d(z))$. Since $\phi$ is join-irreducible, we find that $\phi \leq b(y) \sqcap d(z)$, for some $y\in Y,d\in TZ$ such that $g(y)\leq_{TZ} d$. Let $\bar y = \smin \{y \mid \phi \leq b(y)\}$. Then,

\[\bar y \leq y \implies g(\bar y)\leq_{TZ} g(y) \implies g(y)(z)\leq g(\bar y)(z).\]

Moreover, from above, we have $\phi\leq d(z)$ and $g(y)\leq_{TZ} d$, i.e., $d(z)\leq g(y)(z)$. Thus, from transitivity of $\leq$ we obtain $\phi\leq g(\bar y)(z)$.

§ ADDITIONAL RESULTS

In the first direction of the proof of Theorem <ref>, a
coequaliser of $E\rightrightarrows X\times \Phi$ provided the carrier of the
resulting coalgebra structure. Even though coequalisers in $\pos$ are not
created by the forgetful functor to $\Set$, this one is:
This result is not required for the main result, it is just a
remark. Should it be dropped?
Given a family of relations $R_\varphi \rightrightarrows X$ with
$R_{\varphi'}\supseteq R_\varphi$ for $\varphi' \le \varphi$.

* We have a poset structure $\sqsubseteq$ on $\coprod_{\varphi\in
\Phi}\nicefrac{X}{R_\varphi}$ defined by

\[
\sqsubseteq [x_2]_{\varphi}
\quad:\Longleftrightarrow\quad
\varphi' \le \varphi\text{ and }[x_1]_{\varphi'} \le [x_2]_{\varphi'}
\text{ in }\nicefrac{X}{R_{\varphi'}}.
\]

* One obtains $(\coprod_{\varphi\in \Phi}\nicefrac{X}{R_\varphi},\sqsubseteq)$
as the coequaliser of $\pi_1,\pi_2: E\rightrightarrows X\times \Phi$ with

\[
E := \big\{
\big((x_1,\varphi),(x_2,\varphi) \big)
\mid (x_1,x_2) \in R_\varphi
\big\}.
\]

* For the well-definedness of $\sqsubseteq$, consider $[x_1]_{\varphi'} =
[x_1']_{\varphi'}$ and $[x_2]_{\varphi} = [x_2']_{\varphi}$ and
assume $[x_1]_{\varphi'} \sqsubseteq [x_2]_{\varphi'}$. Then $\varphi' \le
\varphi$ and

\[
\ =\ [x_1]_{\varphi'}
\ =\ [x_2]_{\varphi'}
\overset{R_\varphi \subseteq R_{\varphi'}}{=} [x_2']_{\varphi'}
\]

and so $[x_1']_{\varphi}\sqsubseteq [x_2']_{\varphi}$.

* Reflexivity is clear.

* For antisymmetry, let $[x_1]_{\varphi'} \sqsubseteq [x_2]_\varphi$
and  $[x_1]_{\varphi'} \sqsupseteq [x_2]_\varphi$. Then $\varphi' =
\varphi$ and by antisymmetry in $\nicefrac{X}{R_{\varphi'}}$ furthermore
$[x_1]_{\varphi'} = [x_2]_{\varphi'} \overset{\varphi = \varphi'}{=} [x_2]_{\varphi}$.

* For transitivity assume $[x_0]_{\varphi''}\sqsubseteq
[x_1]_{\varphi'}\sqsubseteq [x_2]_{\varphi}$, then first of all
$\varphi'' \le\varphi'\le \varphi$ and so

\[
[x_1]_{\varphi'} \le [x_2]_{\varphi'}
\Rightarrow
[x_1]_{\varphi''} \le [x_2]_{\varphi''}
\]

and hence $[x_0]_{\varphi''} \le [x_1]_{\varphi''} \le

* The map $\kappa$ with $\kappa(x,\varphi) = [x]_\varphi$ is monotone in $x$ by
the definition of $X\twoheadrightarrow\nicefrac{X}{R_\varphi}$ as a
coequaliser and is monotone in $\varphi$ by the definition of $\sqsubseteq$.
For the universal property, take a montone map $f: X\times \Phi \to Y$
making the projections $E\rightrightarrows X$ equal. We define the map

\[
u: (\coprod_{\varphi\in \Phi}\nicefrac{X}{R_\varphi},\sqsubseteq)
\to Y
,\quad u([x]_\varphi) = f(x,\varphi),
\]

which is well-defined because for $[x_1]_{\varphi} = [x_2]_\varphi$,
$(x_1,\varphi)$ and $(x_2,\varphi)$ are related by $E$ and thus mapped to
the same element by $f$. For monotonicity, let $[x']_{\varphi'}\sqsubseteq
[x]_\varphi$. Then by definition, $\varphi' \le \varphi$ and
$[x']_{\varphi'}\le [x]_{\varphi'}$ in $\nicefrac{X}{R_{\varphi'}}$. For the
inclusion $i: X\to X\times \Phi$, $i(x) = (x,\varphi')$, $f\cdot i$ makes
$R_{\varphi'}\rightrightarrows X$ equal and thus induces a unique monotone
map $\nicefrac{X}{R_{\varphi'}} \to Y$. Hence, $f(x',\varphi') \le
f(x,\varphi')$ and in total $f(x',\varphi') \le f(x,\varphi)$.
For the uniqueness of $u$, consider some $v$ with $v\cdot \kappa = f$ and
$[x]_\varphi$ in $\nicefrac{X}{R_\varphi}$; hence $v([x]_\varphi) =
v(\kappa(x,\varphi)) = f(x,\varphi) = u(x,\varphi)$.

Note that we do not write the order relation explicitly in
$\nicefrac{X}{R_\varphi}$, because it carries the poset structure of coequaliser of $R_\varphi
\rightrightarrows X$ in $\pos$. However, we write $\sqsubseteq$ explicitly,
because it is more than the poset structure of the coproduct $\coprod_{\varphi
\in \Phi} \nicefrac{X}{R_\varphi}$.

If $\Phi$ is not discrete, then $p$ is not monotone in $\Phi$ and thus not
defined in $\pos$. Furthermore, there is no meaningful way to extend $\pow$ to
$\Kl(\arg^\Phi)$, that is, any distributive law completely collapses the poset
order $a \le b$ of $\Phi$, as we show next:
This result is not required for the following counter-example, it is just a
remark, and might even be misleading, because it also true for $\pow(\arg\times\Phi)$. Should it be dropped?  If
$\bar s: \pow \Rightarrow \pow(\arg\times\Phi)^\Phi$ fulfills
$\eqref{sMonadPreservation}$, then for all $a\le b$ b: Replace
$a,b$ by $\phi,\psi,\dots$ in $\Phi$, $X\in \pos$, $M\subseteq X$
we have $\bar s_X(M)(a) = \bar s_X(M)(b)$.

For proving the main result, we will need the following argument:

If $X\in \pos$, $M\subseteq X$, and $(x,\varphi) \in \bar
s_X(M)(a)$ then $(y,\varphi) \in \bar s_{X}(M)(a)$ for all $y\in M$.

Since $\pow \pi_1(\bar s_X(M)(a)) = \nu_X(M)(a) = M$ by
(<ref>), we have that $x\in M$. Denote by $(X,=)$ the poset
with elements from $X$ ordered discretely and by $(X,\le)$ the original order
of $X$ for clarity reasons. Then we have an inclusion $i: (X,=)\hookrightarrow
(X,\le)$. Now for any $y\in M$, the permutation $f: (X,=)\to
(X,=)$ swapping $x$ and $y$ is a monotone map and by naturality of $\bar s$ we

\[
\begin{tikzcd}[row sep=2mm, column sep=12mm]
M \arrow[phantom]{d}[sloped,description]{\in}
\arrow[mapsto]{r}
& M \arrow[phantom]{d}[sloped,description]{\in}
\arrow[mapsto]{r}
& M \arrow[phantom]{d}[sloped,description]{\in}
\\
\pow (X,=)
\arrow{r}{\pow f}
\arrow{d}{\bar s_{(X,=)}}
\pow (X,=)
\arrow{r}{\pow i}
\arrow{d}{\bar s_{(X,=)}}
\pow (X,\le)
\arrow{d}{\bar s_{(X,\le)}}
\\[4mm]
\pow ((X,=)\times \Phi)^\Phi
\arrow{r}{\pow (f\times \Phi)^\Phi}
\pow ((X,=)\times \Phi)^\Phi
\arrow{r}{\pow (i\times \Phi)^\Phi}
\pow ((X,\le)\times \Phi)^\Phi
\end{tikzcd}
\]

The right-hand square shows that $(x,\varphi) \in \bar
s_{(X,=)}(M)(a)$. Applying this fact to the whole diagram proves first that
$(y,\varphi) \in \bar s_{(X,=)}(M)(a)$ and second that
$(y,\varphi) \in \bar s_{(X,\le)}(M)(a)$.

By the monotonicity of $\bar s$, we have directly

\[
\bar s_X(M)(a) \supseteq \bar s_X(M)(b)\quad\text{for all }X\subseteq M.
\]

Conversely, let $ (x,\varphi) \in \bar s_X(M)(a)$. By
(<ref>), $M = \pow(\pi_1)(\bar s(M)(b))$ and so there is
some $\varphi' \in \Phi$ with

\[
(x,\varphi') \in \bar s_{X}(M)(b) \subseteq \bar s_X(M)(a).
\]

Apply Lemma <ref> for $\bar s_X(M)(a) \subseteq
X\times \Phi$ and $((x,\varphi),\varphi) \in \bar s_X(\bar s_X(M)(a))(a)$ in order
to obtain

\[
\forall y \in \bar s_X(M)(a):
(y,\varphi) \in \bar s_X(\bar s_X(M)(a))(a)
\]

Applying this to $(x,\varphi') \in \bar s_X(M)(a)$ one obtains

\[
((x,\varphi'),\varphi) \in \bar s_X(\bar s_X(M)(a))(a).
\]

By (<ref>), $\varphi = \varphi'$ and thus $(x,\varphi) = (x,\varphi') \in
\bar s(M)(b)$.

Concretely $\Lambda$ defines a distributive law $\lambda$ by composition

\[
\lambda_X :\equiv \big(
\xrightarrow{\bar \Lambda_{TX}}
\xrightarrow{TH\epsilon_X}
\big).
\]

The functor extension $\hat H: \Kl(\arg^\Phi) \to \Kl(\arg^\Phi)$ then, for any $f:LX \to Y$, is
defined as:

\begin{equation}
\hat H (Tf\cdot \rho_X: X\kleislito Y)
:\equiv \big(
\xrightarrow{\bar s_X}
\xrightarrow{THf}
\big).
\label{extensionByS}
\end{equation}

Take a functor $H: \C\to \C$ on a cartesian closed category and fix some $\Phi\in \C$. There is a
one-to-one correspondence between distributive laws
$\lambda\colon H(\arg^\Phi)\Rightarrow (H\arg)^\Phi$ and natural
transformations $\bar s: H\Rightarrow H(\arg\times \Phi)^\Phi$

\begin{equation}\label{sMonadPreservation} %
\begin{tikzcd}
H X
\arrow{d}[swap]{\bar s_X}
\arrow{dr}{\nu_{H X}}
\\
H(X\times \Phi)^\Phi
\arrow{r}[swap]{{H \pi_1}^\Phi}
& H(X)^\Phi
\end{tikzcd}
\quad
\begin{tikzcd}[column sep=4mm]
H(X\times \Phi)^\Phi
\arrow{d}[swap]{(\bar s_{X\times \Phi})^\Phi}
& H X
\arrow{r}{\bar s_X}
\arrow{l}[swap]{\bar s_X}
H(X\times \Phi)^\Phi
\arrow{d}{H(X\times \Delta_\Phi)^\Phi}
\\
H(X\times \Phi\times \Phi)^{\Phi\Phi}
\arrow{rr}[swap]{\zeta_{H(X\times \Phi\times \Phi)}}
& H(X\times \Phi\times \Phi)^{\Phi}
\end{tikzcd}
\end{equation}

tw: probably drop this
Given a distributive law $\lambda$, the defined $\bar s_X$ fulfills the first
axiom of (<ref>) by:

\[
\begin{tikzcd}[column sep =14mm]
\arrow{d}[swap]{H\rho_X}
\arrow[shiftarr={xshift=-18mm}]{dd}[swap]{\bar s_X}
\arrow[shift left=1]{dr}[sloped,above]{H\eta_X}
\arrow[
rounded corners,
to path={
-- ([xshift=5mm]\tikztotarget.east |- \tikztostart.east)
-- ([xshift=5mm]\tikztotarget.east)
-- (\tikztotarget.east)
\descto[xshift=16mm]{dr}{distributive\\law}
\descto[xshift=-7mm]{dr}{(Def. $\eta$)}
\\
\arrow{d}[swap]{\lambda_{LX}}
\arrow{r}{{HT\vartheta_X}}
\descto{dr}{Naturality\\ of $\lambda$}
&|[alias=corner]| HTX
\arrow{d}{\lambda_X}
\\
\arrow{r}[swap]{TH\vartheta_X}
& THX
\end{tikzcd}
\]

The second axiom in (<ref>) is fulfilled by:

\[
\begin{tikzcd}[column sep = 4mm]
\arrow{d}[swap]{TH\rho_{LX}}
\descto{dr}{Naturality\\ of $\lambda$}
& HTLX
\arrow{l}[swap]{\lambda_{LX}}
\arrow{d}{HT\rho_{LX}}
& HX
\arrow{r}[yshift=1mm]{H\rho_X}
\arrow{l}[swap,yshift=1mm]{H\rho_X}
\descto{d}{(Def. $\mu$)}
& HTLX
\arrow{r}{\lambda_{LX}}
\arrow{d}[swap]{HT\delta_X}%{H(X\times \Delta_\Phi)^\Phi}
\descto[xshift=4mm,yshift=2mm]{ddr}{Naturality\\ of $\lambda$}
& THLX
\arrow{dd}[sloped,above]{TH\delta_X}
\\
\arrow{d}{T\lambda_{LLX}}
& HTTLLX
\arrow{rr}[swap]{H\mu_{LLX}}
\arrow{l}[yshift=-1mm,pos=0.0]{\lambda_{TLLX}}
& {} & HTLLX
\arrow{dr}[sloped,below]{\lambda_{LLX}}
\\
\arrow{rrrr}{\mu_{HLLX}}
& & {} \descto{u}{distributive law $\lambda$} &&
\end{tikzcd}
\]

Given a natural transformation $\bar s$ with (<ref>), then
the unit $\eta$ is preserved by $\lambda$:

\[
\begin{tikzcd}[column sep=18mm]
H X
\arrow{d}[swap]{H\eta_X}
\arrow{r}{\bar s_X}
\arrow[
rounded corners,
to path={
-- ([yshift=2mm]\tikztostart.north)
-- ([yshift=2mm,xshift=14mm] corner.north east |- \tikztostart.north)
%-- ([yshift=3mm]\tikztotarget.north)
-- (\tikztotarget) \tikztonodes
]{drr}{\eta_{H X}}
\descto[xshift=-3mm]{dr}{Naturality\\ of $\bar s$}
&|[alias=corner]| THLX
\arrow{d}[swap]{THL\eta_X}
\arrow[bend left=10]{dr}[sloped,above,pos=0.8]{TH\vartheta_X}
\descto[xshift=-8mm]{dr}{(Def. $\eta$)}
\descto[pos=0.4]{r}{\eqref{sMonadPreservation}}
& {}
\\
\arrow{r}[swap]{\bar s_{TX}}
& THL TX
\arrow{r}[swap]{TH\epsilon_X}
& THX
\end{tikzcd}
\]

For the preservation of multiplication $\mu$ see Figure <ref>.
column sep=2mm,
rounded corners,
to path=
– ([yshift=6mm].north)
– ($ (\tikztotarget -| \tikztostart) !.6! (\tikztotarget) $)
– ()
baseline=($ (current bounding box.south) + (0,0mm) $),
of $\bar s$

H TTX
ddr[swap]H μ_X

T THL LTTX
ur[sloped,above,pos=0.3]TTHL ϵ_TX
of $\mu$

of $\mu$
ddlμ_H X

|[yshift=5mm,inner sep=1mm]| THLTTX
[bend right=0]r[pos=0.0,yshift=0mm]THδ_TTX
[bend right=0]dr[sloped,below,pos=0.5]THLμ_X
of $\bar s$
d(Def. $\mu$)

|[xshift=-10mm]| HTX
|[xshift=-10mm]| THLTX
|[alias=lastrow,xshift=15mm]| THX

The pentagonal law in the proof of Lemma <ref>

Lastly, for an arrow $LX \xrightarrow f Y$ we have

\begin{align*}
\hat H (Tf\cdot \rho_X) &= \lambda_Y \cdot H(Tf\cdot \rho_X)
= \lambda_Y \cdot HTf \cdot H\rho_X \quad \text{(Naturality of $\lambda$)}\\
&= THf \cdot \lambda_{LX} \cdot H\rho_X = THf \cdot \bar s_X.\tag*{\qEd}
\end{align*}