1: \begin{definition}[$\bbP^{\rho}$, $\bbP^{(\tau, \rho)}$]

2:   \label{def:alternating-pred-transf}

3:   Let $T$ be a monad on $\Set$, $\cat{D}$ be a complete category

4:   and $\bar{\Omega} = (\OmegaD, \tau)$ be a $\cat{D}$-relative $T$-algebra.

5:   Moreover let $R$ be a monad on $\EM(T)$

6:   and $\rho \colon R \to [[\place , \bar{\Omega}]_{T} , \bar{\Omega}]_{\cat{D}}$ be a monad map.

7:   Here $[[\place , \bar{\Omega}]_{T} , \bar{\Omega}]_{\cat{D}}$ is the monad

8:   that arises from the dual adjunction

9:   \begin{math}

10:     \xymatrix@1@C-.5em{

11:       {\EM(T)}

12:         \ar@/^.4em/[r]

13:         \ar@{}[r]|-{\bot}

14:       &

15:       {\cat{D}^{\op}}

16:         \ar@/^.4em/[l]

17:     }

18:   \end{math}

19:   induced by $\bar{\Omega}$ as in Theorem~\ref{thm:state-effect-triangle-relative}.

20: 

21:  We define a functor $\bbP^{\rho} \colon \Kl(R) \to \cat{D}^{\op}$

22:  by:

23:   $\bbP^{\rho} A_a = A_a$ and

24:   \begin{align*}

25: %    \bbP^{\rho} A_a &= A_a \enspace, \quad \text{and} \\

26:     \bbP^{\rho}(A_a \stackrel{f}{\to} B_b

27:  \text{ in $\Kl(R)$}

28: )

29:       &= \bigl(\,[B_b, \bar{\Omega}]_{T} \stackrel{\rho^{\sharp}}{\to}

30:           [R B_b, \bar{\Omega}]_{T} \stackrel{f^*}{\to}

31:             [A_a, \bar{\Omega}]_{T} \,\bigr)\enspace .

32:   \end{align*}

33:  Furthermore,

34: by  precomposing

35: % $\bbP^{\rho} \colon \Kl(R) \to \cat{D}^{\op}$ and

36:  the comparison functor $K \colon \Kl(R \star T) \to \Kl(R)$,

37:   we have another functor:

38:   \begin{equation}

39:     \bbP^{(\tau, \rho)} = \bbP^{\rho} \co K \;\colon\; \Kl(R \star T) \longto \cat{D}^{\op}

40:     \enspace .

41:   \end{equation}

42: \end{definition}

43: