\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{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{remark}
The above function is injective but not surjective; there are effectoids that do not correspond to preordered monoids.
\end{remark}

\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}

\end{document}