\documentclass{article}
\input{packages}
\input{def}

\pdfmapline{=rossbb rossbb <rossbb.pfb}
\DeclareSymbolFont{rossbb}{T1}{rossbb}{m}{n}
\DeclareMathSymbol{\bbepsilon}{\mathord}{rossbb}{`e}
\DeclareMathSymbol{\bbsemicolon}{\mathpunct}{rossbb}{`;}

\newcommand{\seq}{\mathop{\bbsemicolon}}

\homework{Effects}

\begin{document}
\maketitle

\begin{exercise}
Prove that the functor $I : \cat{C} \mto \cat{Eff}(\alg{M})$ for any monad~$\alg{M}$ on a category~$\cat{C}$ has a right adjoint~$R$ such that the process for building a monad out of the adjunction $I \dashv R$ results in $\alg{M}$.
($I$ is given in Exercise~2 of the Kliesli Categories lecture notes. You may assume $I$ is distributive and preserves identities.)

To maintain sanity, use $\id$ and $\cocomp$ for identity and composition in $\cat{C}$, and use $\id^*$ and $\cocomp^*$ for identity and composition in $\cat{Eff}(\alg{M})$.
Similarly, if $\mo{f} : \ob{C}_1 \mto M(\ob{C}_2)$ is a morphism in $\cat{C}$, then $\mo{f}^* : \ob{C}_1 \mto^* \ob{C}_2$ is the corresponding morphism in $\cat{Eff}(\alg{M})$.
\end{exercise}

\begin{proof}
Let $R$ map $\ob{C}$ to $M(\ob{C})$ and $\mo{f}^* : \ob{C}_1 \mto^* \ob{C}_2$ to $M(\mo{f}) \cocomp \mu_{\ob{C}_2}$.
The identity of $\ob{C}$ gets mapped to $M(\id_\ob{C}^*) \cocomp \mu_\ob{C}$, which equals the identity since $\id^* = \eta$ is an identity of $\mu$.
The composition $\mo{f}^* \cocomp^* \mo{g}^*$ gets mapped to $M(\mo{f} \cocomp M(\mo{g}) \cocomp \mu) \cocomp \mu$, which equals $M(\mo{f}) \cocomp M(M(\mo{g})) \cocomp M(\mu) \cocomp \mu$ by distributivity of~$M$, which equals $M(\mo{f}) \cocomp M(M(\mo{g})) \cocomp \mu \cocomp \mu$ by associativity of $\mu$, which equals $M(\mo{f}) \cocomp \mu \cocomp M(\mo{g}) \cocomp \mu$ by naturality of $\mu$, which is the composition of what $\mo{f}^*$ and $\mo{g}^*$ each get mapped to.
Thus, $R$ is a functor.

$I$ maps the object $\ob{C}$ to $\ob{C}$, which $R$ maps to $M(\ob{C})$.
$I$ maps the morphism $\mo{f}$ to $(\mo{f} \cocomp \eta)^*$, which $R$ maps to $M(\mo{f} \cocomp \eta) \cocomp \mu$, which equals $M(\mo{f}) \cocomp M(\eta) \cocomp \mu$, which equals $M(\mo{f})$ because $\eta$ is an identity of $\mu$.
Thus, $I \cocomp R$ equals $M$.

The unit of the adjunction is simply the unit of the monad.
The counit $\varepsilon : R \cocomp I \nto \cat{Eff}(\alg{M})$ is the natural transformation mapping each object $\ob{C}$ to the morphism $(\id_{M(\ob{C})})^* : I(R(\ob{C})) = M(\ob{C}) \mto^* \ob{C}$, which is natural because $I(R(\mo{f}^*)) \cocomp^* \varepsilon_{\ob{C}_2}$ is defined as $(M(\mo{f}) \cocomp \mu_{\ob{C}_2} \cocomp \eta_{M(\ob{C}_2)})^* \cocomp^* (\id_{M(\ob{C}_2)})^* = (M(\mo{f}) \cocomp \mu_{\ob{C}_2} \cocomp \eta_{M(\ob{C}_2)} \cocomp M(\id_{M(\ob{C}_2)}) \cocomp \mu_{\ob{C}_2})^*$ which equals $(\id_{M(\ob{C}_1)} \cocomp M(\mo{f}) \cocomp \mu_{\ob{C}_2})^*$, the definition of $\varepsilon_{\ob{C}_1} \cocomp^* \mo{f}^*$, since $M$ preserves identities and $\eta$ is an identity of $\mu$.

Finally, $I(\eta_\ob{C}) \cocomp^* \varepsilon_{I(\ob{C})}$ is defined as $(\eta_\ob{C} \cocomp \eta_{M(\ob{C})})^* \cocomp^* (\id_{M(\ob{C})})^*$, which is defined as $(\eta_\ob{C} \cocomp \eta_{M(\ob{C})} \cocomp M(\id_{M(\ob{C})}) \cocomp \mu_\ob{C})^*$, which equals $(\eta_\ob{C})^*$ because $\eta$ is an identity of $\mu$, which is the definition of $\id^*_{I(\ob{C})}$.
And, $\eta_{R(\ob{C})} \cocomp R(\varepsilon_\ob{C})$ is defined as $\eta_{M(\ob{C})} \cocomp M(\id_{M(\ob{C})}) \cocomp \mu_\ob{C}$, which equals $\id_{R(\ob{C})}$ because $M$ preserves identities and $\eta$ is an identity of $\mu$.
\end{proof}

\begin{exercise}
Preordered monoids are the internal monoids of $\cat{Prost}$.
Prove that there is a function from the set of preordered monoids to the set of effectoids such that the set of the effects of an output of this function is the underlying set of the corresponding input.
\end{exercise}

\begin{proof}
Let $\langle E, \seq, \noprf, \bbepsilon, \noprf, \leq, \noprf \rangle$ be a preordered monoid.
Define $\bbepsilon \mapsto \varepsilon$ to be $\bbepsilon \leq \varepsilon$.
Define $\varepsilon_1 \seq \varepsilon_2 \mapsto \varepsilon$ to be $\varepsilon_1 \seq \mapsto \varepsilon_2 \leq \varepsilon$.
This, along with $\leq$, defines an effectoid with the effect set $E$; all we have to do is prove the required properties.
\begin{description}
\item[Identity] Suppose we have $\varepsilon, \varepsilon' : E$. If there exists $\varepsilon_\ell$ such that $\bbepsilon \leq \varepsilon_\ell$ and $\varepsilon_\ell \seq \varepsilon \leq \varepsilon'$, then due to identity and congruence and exploiting transitivity we have $\varepsilon = \bbepsilon \seq \varepsilon \leq \varepsilon_\ell \seq \varepsilon \leq \varepsilon'$. If $\varepsilon \leq \varepsilon'$, then if we define $\varepsilon_\ell$ to be $\bbepsilon$ we know that $\bbepsilon \leq \varepsilon_\ell$ by reflexivity and $\varepsilon_\ell \seq \varepsilon = \varepsilon \leq \varepsilon'$ by identity. Similar arguments apply for right identity.
\item[Associativity] Suppose we have $\varepsilon_1, \varepsilon_2, \varepsilon_3, \varepsilon : E$. If there exists some $\bar{\varepsilon}$ such that $\varepsilon_1 \seq \varepsilon_2 \leq \bar{\varepsilon}$ and $\bar{\varepsilon} \seq \varepsilon_3 \leq \varepsilon$, then we can define $\hat{\varepsilon}$ to be $\varepsilon_2 \seq \varepsilon_3$ so that $\varepsilon_2 \seq \varepsilon_3 \leq \hat{\varepsilon}$ holds by reflexivity and, exploiting transitivity, $\varepsilon_1 \seq \hat{\varepsilon} = (\varepsilon_1 \seq \varepsilon_2) \seq \varepsilon_3 \leq \bar{\varepsilon} \seq \varepsilon_3 \leq \varepsilon$ holds due to associativity and congruence. A similar argument holds for the reverse implication.
\item[Reflexivity] Holds by definition of preorder.
\item[Congruence] Holds due to transitivity and the definition of $\bbepsilon \mapsto \varepsilon$ and $\varepsilon_1 \seq \varepsilon_2 \mapsto \varepsilon$.
\end{description}
\end{proof}

\begin{exercise}
Suppose that we want to build a productoid for the effectoid arising from the preorderd monoid $\Set(\{1,2\})_{\subseteq,\cup}$.
Because this monoid is idempotent, it turns out any such productoid would provide a monadic structure (i.e.~unit and join) for each $\mo{m}_\varepsilon$.
Suppose we want to require the monad for $\mo{m}_\varnothing$ to be the identity monad (meaning the identity 1-cell with identity 2-cells for unit and join).
Suppose furthermore we want to require $\mo{m}_{\{1,2\}}$ to equal $\mo{m}_{\{1\}} \cocomp \mo{m}_{\{2\}}$ and require $\mu_{\{1\} \cup \{2\}}^{\{1,2\}}$ to be the identity 2-cell of $\mo{m}_{\{1\}} \cocomp \mo{m}_{\{2\}}$.
Let $\mo{m}_1$ denote $\mo{m}_{\{1\}}$ and $\mo{m}_2$ denote $\mo{m}_{\{2\}}$.
It turns out that building such a productoid would require just one more 2-cell $\delta : \mo{m}_2 \cocomp \mo{m}_1 \nto \mo{m}_1 \cocomp \mo{m}_2$ satisfying four equations (without needing to use universal quantifiers).
Determine what these four equations are, though do not provide the proof that they are necessary and sufficient to build a productiod satisfying the required property.
Hint: $\delta$ corresponds to $\mu_{\{2\} \cup \{1\}}^{\{1,2\}}$. Also, save time by copy-pasting the diagrams from the lecture notes.
\end{exercise}

\begin{proof}
Let $\eta_1$ and $\mu_1$ denote the unit and join for $\mo{m}_1$, and let $\eta_2$ and $\mu_2$ denote the unit and join for $\mo{m}_2$.\\
\begin{tikzpicture}[baseline=(c1.base)]
\node(c1) at (0,0) {$\ob{C}$};
\node(c2) at (4,0) {$\ob{C}$};
\draw[->] (c1) .. controls (1.5,-1.5) and (2.5,-1.5) .. node(f1){} node[below]{$\mo{m}_2$} (c2);
\draw[->] (c2) .. controls (1.75,-1.75) and (1.75,1.75) .. node(f2){} node[left]{$\mo{m}_1$} (c2);
\draw[->] (c1) .. controls (1.5,1.5) and (2.5,1.5) .. node(f12){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c2);
\draw[double,double equal sign distance,-implies] (c2) -- node[above]{$\eta_1$} (f2);
\draw[double,double equal sign distance,-implies] ($(f1.west) !.5! (c2.south)$) .. controls +(-2,-.5) and ($(f12.south west) + (-1,-1)$) .. node[above left]{$\delta$} (f12.south west);
\end{tikzpicture}
must equal
\begin{tikzpicture}[baseline=(c1.base)]
\node(c1) at (0,0) {$\ob{C}$};
\node(c2) at (4,0) {$\ob{C}$};
\draw[->] (c1) .. controls (2.25,1.75) and (2.25,-1.75) .. node(f1){} node[right]{$\mo{m}_1$} (c1);
\draw[->] (c1) .. controls (1.5,-1.5) and (2.5,-1.5) .. node(f2){} node[below]{$\mo{m}_2$} (c2);
\draw[->] (c1) .. controls (1.5,1.5) and (2.5,1.5) .. node(f12){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c2);
\draw[double,double equal sign distance,-implies] (c1) -- node[above]{$\eta_1$} (f1);
\draw[double,double equal sign distance] ($(f2.east) !.5! (c1.south)$) .. controls +(2,-.5) and ($(f12.south east) + (1,-1)$) .. (f12.south east);
\end{tikzpicture}
since both must equal $\mu_{\{2\} \subseteq}^{\{1,2\}}$.\\
\begin{tikzpicture}[baseline=(c1.base)]
\node(c1) at (0,0) {$\ob{C}$};
\node(c2) at (4,0) {$\ob{C}$};
\draw[->] (c1) .. controls (2.25,1.75) and (2.25,-1.75) .. node(f1){} node[right]{$\mo{m}_2$} (c1);
\draw[->] (c1) .. controls (1.5,-1.5) and (2.5,-1.5) .. node(f2){} node[below]{$\mo{m}_1$} (c2);
\draw[->] (c1) .. controls (1.5,1.5) and (2.5,1.5) .. node(f12){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c2);
\draw[double,double equal sign distance,-implies] (c1) -- node[above]{$\eta_2$} (f1);
\draw[double,double equal sign distance,-implies] ($(f2.east) !.5! (c1.south)$) .. controls +(2,-.5) and ($(f12.south east) + (1,-1)$) .. node[above right]{$\delta$} (f12.south east);
\end{tikzpicture}
must equal
\begin{tikzpicture}[baseline=(c1.base)]
\node(c1) at (0,0) {$\ob{C}$};
\node(c2) at (4,0) {$\ob{C}$};
\draw[->] (c1) .. controls (1.5,-1.5) and (2.5,-1.5) .. node(f1){} node[below]{$\mo{m}_1$} (c2);
\draw[->] (c2) .. controls (1.75,-1.75) and (1.75,1.75) .. node(f2){} node[left]{$\mo{m}_2$} (c2);
\draw[->] (c1) .. controls (1.5,1.5) and (2.5,1.5) .. node(f12){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c2);
\draw[double,double equal sign distance,-implies] (c2) -- node[above]{$\eta_2$} (f2);
\draw[double,double equal sign distance] ($(f1.west) !.5! (c2.south)$) .. controls +(-2,-.5) and ($(f12.south west) + (-1,-1)$) .. (f12.south west);
\end{tikzpicture}
since both must equal $\mu_{\{1\} \subseteq}^{\{1,2\}}$.\\
\begin{tikzpicture}[baseline=0]
\node(c1) at (0,1) {$\ob{C}$};
\node(c2) at (1,-1) {$\ob{C}$};
\node(c3) at (3,-1) {$\ob{C}$};
\node(c4) at (4,1) {$\ob{C}$};
\draw[->] (c1) -- node[below left]{$\mo{m}_2$} (c2);
\draw[->] (c2) -- node[below]{$\mo{m}_2$} (c3);
\draw[->] (c3) -- node[below right]{$\mo{m}_1$} (c4);
\draw[->] (c1) -- node(f12){} node[above]{$\mo{m}_2$} (c3);
\draw[->] (c1) -- node(f123){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c4);
\draw[double,double equal sign distance,-implies] (c2) -- node[below right]{$\mu_2$} (f12);
\draw[double,double equal sign distance,-implies] (c3) -- node[above right]{$\delta$} (f123);
\end{tikzpicture}
must equal
\begin{tikzpicture}[baseline=0]
\node(c1) at (0,1) {$\ob{C}$};
\node(c2) at (1,-1) {$\ob{C}$};
\node(c3) at (3,-1) {$\ob{C}$};
\node(c4) at (4,1) {$\ob{C}$};
\node(c5) at ($(c2)!.5!(c4)$) {$\ob{C}$};
\node(c6) at (2,1) {$\ob{C}$};
\draw[->] (c1) -- node[below left]{$\mo{m}_2$} (c2);
\draw[->] (c2) -- node[below]{$\mo{m}_2$} (c3);
\draw[->] (c3) -- node[below right]{$\mo{m}_1$} (c4);
\draw[->] (c2) -- node[below,sloped]{$\mo{m}_1$} (c5);
\draw[->] (c5) -- node[below,sloped]{$\mo{m}_2$} (c4);
\draw[->] (c1) -- node[above]{$\mo{m}_1$} (c6);
\draw[->] (c6) -- node(f){} node[above]{$\mo{m}_2$} (c4);
\draw[->] (c6) -- node[below,sloped]{$\mo{m}_2$} (c5);
\draw[double,double equal sign distance,-implies] (c3) -- node[below left]{$\delta$} (c5);
\draw[double,double equal sign distance,-implies] (c2) -- node[above left]{$\delta$} (c6);
\draw[double,double equal sign distance,-implies] (c5) -- node[right,near end]{$\mu_2$} (f);
\end{tikzpicture}
.\\
\begin{tikzpicture}[baseline=0]
\node(c1) at (0,1) {$\ob{C}$};
\node(c2) at (1,-1) {$\ob{C}$};
\node(c3) at (3,-1) {$\ob{C}$};
\node(c4) at (4,1) {$\ob{C}$};
\draw[->] (c1) -- node[below left]{$\mo{m}_2$} (c2);
\draw[->] (c2) -- node[below]{$\mo{m}_1$} (c3);
\draw[->] (c3) -- node[below right]{$\mo{m}_1$} (c4);
\draw[->] (c2) -- node(f23){} node[above]{$\mo{m}_1$} (c4);
\draw[->] (c1) -- node(f123){} node[above]{$\mo{m}_1 \cocomp \mo{m}_2$} (c4);
\draw[double,double equal sign distance,-implies] (c3) -- node[below left]{$\mu_1$} (f23);
\draw[double,double equal sign distance,-implies] (c2) -- node[above left]{$\delta$} (f123);
\end{tikzpicture}
must equal
\begin{tikzpicture}[baseline=0]
\node(c1) at (0,1) {$\ob{C}$};
\node(c2) at (-1,-1) {$\ob{C}$};
\node(c3) at (-3,-1) {$\ob{C}$};
\node(c4) at (-4,1) {$\ob{C}$};
\node(c5) at ($(c2)!.5!(c4)$) {$\ob{C}$};
\node(c6) at (-2,1) {$\ob{C}$};
\draw[<-] (c1) -- node[below right]{$\mo{m}_1$} (c2);
\draw[<-] (c2) -- node[below]{$\mo{m}_1$} (c3);
\draw[<-] (c3) -- node[below left]{$\mo{m}_2$} (c4);
\draw[<-] (c2) -- node[below,sloped]{$\mo{m}_2$} (c5);
\draw[<-] (c5) -- node[below,sloped]{$\mo{m}_1$} (c4);
\draw[<-] (c1) -- node[above]{$\mo{m}_2$} (c6);
\draw[<-] (c6) -- node(f){} node[above]{$\mo{m}_1$} (c4);
\draw[<-] (c6) -- node[below,sloped]{$\mo{m}_1$} (c5);
\draw[double,double equal sign distance,-implies] (c3) -- node[below right]{$\delta$} (c5);
\draw[double,double equal sign distance,-implies] (c2) -- node[above right]{$\delta$} (c6);
\draw[double,double equal sign distance,-implies] (c5) -- node[left,near end]{$\mu_1$} (f);
\end{tikzpicture}
.
\end{proof}

\end{document}