\documentclass[10pt,letterpaper]{article}
\usepackage{latexsym}
\input homework
\def\C{{\bf C}}
\def\nc{\triangle}
\def\fst{{\rm fst}}
\def\snd{{\rm snd}}
\author{Jason Reed}
\title{Priorities and Comonads}
\date{November 18, 2000}
\begin{document}
\maketitle
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\section{Priorities and Comonads}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{definition} A {\em priority} on a category $\C$ with finite limits is a pair $(P,\sigma)$
where $P$ is a lex endofunctor on $\C$ and $\sigma$ is a natural transformation $P\to P^2$
such that the diagram
\begin{diagram}
P^3&\lTo^{\sigma_P}&P^2\cr
\uTo<{P\sigma}&&\uTo>\sigma&&(i)\cr
P^2&\lTo_\sigma&P\cr
\end{diagram}
commutes, and the diagram
\begin{diagram}
P^2(X\times Y)&\lTo^{\sigma_{X\times Y}}&P(X\times Y)\cr
\uTo<{Pq_{XY}}\cr
P(PX \times PY)&&\uTo>{q_{XY}}&&(ii)\cr
\uTo<{q_{PX,PY}}\cr
P^2X \times P^2Y&\lTo_{\sigma_X \times \sigma_Y}&PX \times PY\cr
\end{diagram}
commutes for any objects $X,Y$ of $\C$, where $q_{XY}$ is the canonical natural isomorphism
$ PX \times PY\to P(X\times Y) $ induced by $P$ being lex.
\end{definition}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{lemma}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Let $(P,\sigma)$ be a priority on a category $\C$. Then the diagram
\begin{diagram}
PA&\rTo^{\sigma_A}&P^2A&\rTo^{P(\sigma_A,1_{PA})}&PTPA\cr
\dTo<{(\sigma_A,1_{PA})}&&&&\dTo>{Pq_{PA,A}}\cr
TPA&\rTo_{q_{PA,A}}&PTA&\rTo_{\sigma_{TA}}&P^2TA\cr
\end{diagram}
commutes.
\label{commute}
\end{lemma}
\begin{proof}
We first observe that
\begin{eqnarray*}
(P\fst_{TPA})P(\sigma_A,1_{PA})\sigma_A &=&  P(\fst_{TPA}(\sigma_A,1_{PA}))\sigma_A\cr
 &=&  P\sigma_A\sigma_A\cr
 &=&  P\sigma_A\fst_{TPA}(\sigma_A, 1_{PA})\cr
 &=&  \fst_{TP^2A}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})\cr
 &=&  (P\fst_{TPA})q_{P^2A,PA}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})\cr
\end{eqnarray*}
and
\begin{eqnarray*}
(P\snd_{TPA})P(\sigma_A,1_{PA})\sigma_A &=&  P(\snd_{TPA}(\sigma_A,1_{PA}))\sigma_A\cr
 &=&  \sigma_A\cr
 &=&  \sigma_A\snd_{TPA}(\sigma_A, 1_{PA})\cr
 &=&  \snd_{TP^2A}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})\cr
 &=&  (P\snd_{TPA})q_{P^2A,PA}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})\cr
\end{eqnarray*}
hence (by pairing the two equations) if we set $h := (P\fst_{TPA},P\snd_{TPA})$ we have
$h P(\sigma_A,1_{PA})\sigma_A = h q_{P^2A,PA}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})$.
But it is easily seen that $h = q^{-1}$, so $h$ is mono and therefore 
$P(\sigma_A,1_{PA})\sigma_A = q_{P^2A,PA}(P\sigma_A\times \sigma_A)(\sigma_A, 1_{PA})$.
Now if we take the diagram $(i)$ and multiply it with the (trivially commutative) diagram
\begin{diagram}
PA&\rTo^{1_{PA}}&PA\cr
\dTo<{1_{PA}}&&\dTo>{\sigma_A}\cr
PA&\rTo_{\sigma_A}&P^2A\cr
\end{diagram}
we obtain
\begin{diagram}
PA\times PA&\rTo^{\sigma_A\times PA}&TPA\cr
\dTo<{\sigma_A\times PA}&&\dTo>{\sigma_{PA}\times\sigma_A}\cr
TPA&\rTo_{P\sigma_{A}\times\sigma_A}&TP^2A\cr
\end{diagram}
and since $(\sigma_A \times PA)\Delta_{PA} = (\sigma_A,1_{PA})$, we have that the diagram
\begin{diagram}
PA&\rTo^{(\sigma_A, PA)}&TPA\cr
\dTo<{(\sigma_A, PA)}&&\dTo>{\sigma_{PA}\times\sigma_A}\cr
TPA&\rTo_{P\sigma_{A}\times\sigma_A}&TP^2A\cr
\end{diagram}
commutes. Putting all of the above together with diagram $(ii)$ with $X := PA$ and $Y := A$, we obtain
the commutativity of
\begin{diagram}[PostScript=dvips]
PA&&\rTo^{\sigma_A}&&P^2A\cr
&\rdTo~{(\sigma_A,1_{PA})}&&&\cr
&&TPA&&\dTo>{P(\sigma_A,1_{PA})}\cr
\dTo<{(\sigma_A,1_{PA})}&&\dTo<{P\sigma_A\times \sigma_A}&\cr
TPA&\rTo_{\sigma_{PA}\times \sigma_A}&TP^2A&\rTo_{q_{P^2A,PA}}&PTPA\cr
\dTo<{q_{PA,A}}&&&&\dTo>{Pq_{PA,A}}\cr
PTA&&\rTo_{\sigma_{TA}}&&P^2TA\cr
\end{diagram}
as required.\cqed
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{theorem}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Let $(P,\sigma)$ be a priority on a category $\C$. If we make the definitions
\begin{eqnarray*}
TA&:=&PA\times A\cr
\epsilon_A&:=&\snd_{PA\times A}\cr
\delta_A&:=&(q_{PA,A} (\sigma_A,1_{PA})\times (PA\times A) )a_{PA,PA,A}(\Delta_{PA}\times A)\cr
\end{eqnarray*}
(where $\Delta_A := (1_A,1_A)$ and $a_{ABC}$ is the canonical natural isomorphism
$(A\times B)\times C \to A\times(B\times C)$) then $(T,\epsilon,\delta)$ is a comonad.
\end{theorem}
\begin{proof}
We easily have that $\epsilon$ and $\delta$ are natural because `everything in sight' is natural in their definition.
To simplify future computations, we define
\begin{eqnarray*}
\alpha_A&:=&(q_{PA,A} (\sigma_A,1_{PA})\times (PA\times A) )\cr
\beta_A&:=&a_{PA,PA,A}\cr
\gamma_A&:=&\Delta_{PA}\times A\cr
\end{eqnarray*}
so that $\delta = \alpha\beta\gamma$. It remains to show that the comonad equalities are satisfied.
We see first that the diagram
\begin{diagram}
TA&\lTo^{\snd_{T^2A}}&T^2A&\rTo^{T\snd_{TA}}&TA\cr
&\luTo<{1_{TA}}&\uTo~{\delta_A}&\ruTo>{1_{TA}}&&(*)\cr
&&TA\cr
\end{diagram}
commutes, because
\begin{eqnarray*}
\snd_{T^2A} \delta_A &=&\snd_{T^2A}\alpha_A \beta_A \gamma_A \cr
&=&\snd_{PA\times (PA\times A)}\beta_A \gamma_A \cr
&=&(\fst_{PA\times A}\snd_{PA\times (PA\times A)},\snd_{PA\times A}\snd_{PA\times (PA\times A)})\beta_A \gamma_A \cr
&=&(\fst_{PA\times A}\snd_{PA\times (PA\times A)}\beta_A,\snd_{PA\times A}\snd_{PA\times (PA\times A)}\beta_A) \gamma_A \cr
&=&(\snd_{PA\times PA}\fst_{(PA\times PA)\times A},\snd_{(PA\times PA)\times A}) \gamma_A \cr
&=&(\snd_{PA\times PA}\fst_{(PA\times PA)\times A} \gamma_A,\snd_{(PA\times PA)\times A} \gamma_A) \cr
&=&(\snd_{PA\times PA}\Delta_{PA}\fst_{PA\times A} ,\snd_{PA\times A} ) \cr
&=&(\fst_{PA\times A} ,\snd_{PA\times A} ) \cr
&=&1_{PA\times A}\cr
\end{eqnarray*}
and
\begin{eqnarray*}
(T\epsilon_{A}) \delta_A &=& T\snd_{TA}\alpha_A \beta_A \gamma_A\cr
&=& (P\snd_{TA} \times \snd_{TA}) \alpha_A \beta_A \gamma_A\cr
&=& (P\snd_{TA}q_{PA,A} (\sigma_A,1_{PA}) \times \snd_{TA})  \beta_A \gamma_A\cr
&=& (\snd_{P^2A\times PA} (\sigma_A,1_{PA}) \times \snd_{TA})  \beta_A \gamma_A\cr
&=& ( 1_{PA} \times \snd_{TA})  \beta_A \gamma_A\cr
&=& ( \fst_{PA\times (PA\times A)} , \snd_{PA\times A}\snd_{PA\times (PA\times A)})  \beta_A \gamma_A\cr
&=& ( \fst_{PA\times (PA\times A)} \beta_A , \snd_{PA\times A}\snd_{PA\times (PA\times A)}\beta_A )  \gamma_A\cr
&=& ( \fst_{PA\times PA}\fst_{(PA\times PA)\times A}  , \snd_{(PA\times PA)\times A} )  \gamma_A\cr
&=& ( \fst_{PA\times PA}\fst_{(PA\times PA)\times A} \gamma_A  , \snd_{(PA\times PA)\times A} \gamma_A ) \cr
&=& ( \fst_{PA\times PA}\Delta_{PA}\fst_{ PA\times A}   , \snd_{ PA\times A}  ) \cr
&=& ( \fst_{ PA\times A}   , \snd_{ PA\times A}  ) \cr
&=& 1_{ PA\times A}\cr
\end{eqnarray*}
This immediately provides that $\epsilon$ behaves correctly as a counit.
Now we want to show that $\delta_T\delta = (T\delta)\delta$.
If we hit the left triangle of $(*)$ `on the inside' with $T$, we see that the following diagram commutes:
\begin{diagram}
T^2A&\lTo^{\snd_{T^3A}}&T^3A\cr
&\luTo<{1_{T^2A}}&\uTo>{\delta_{TA}}&&(**)\cr
&&T^2A\cr
\end{diagram}
We can then verify that $\snd_{T^3}\delta_{TA}\delta_A = \snd_{T^3}(T\delta_A)\delta_A$ by
chasing the diagram resulting from pasting together $(**)$ with the left triangle of $(*)$ and
the naturality of $\snd$ and $1_\C$:
\begin{diagram}
&&TA&&\cr
&\ldTo^{\delta_A}&\dTo~{1_{TA}}&\rdTo^{\delta_A}\cr
T^2A&&TA&\lTo_{\snd_{T^2A}}&T^2A\cr
\dTo<{\delta_{TA}}&\rdTo~{1_{T^2A}}&\dTo~{\delta_A}&&\dTo>{T(\delta_A)}\cr
T^3A&\rTo_{\snd_{T^3A}}&T^2A&\lTo_{\snd_{T^3A}}&T^3A\cr
\end{diagram}

Next we observe that $\fst_{T^2A}\delta_A = q_{PA,A}(\sigma_A,1_{PA})\fst_{TA}$, for the following diagram commutes:
\begin{diagram}[PostScript=dvips]
TA&&&\rTo^{\delta_{A}}&&&T^2A\cr
&\rdTo~{\gamma_{A}}&&&&\ruTo~{\alpha_{A}}\cr
&&(PA)^2\times A&\rTo^{\beta_{A}}&PA\times TA&&\cr
\dTo~{\fst_{TA}}&&\dTo~{\fst_{(PA)^2 \times A}}&&\dTo~{\fst_{PA\times TA}}&&\dTo~{\fst_{T^2A}}\cr
   &                    &(PA)^2       &                      &   &   &PTA\cr
   &\ruTo~{\Delta_{PA}}&              &\rdTo~{\fst_{(PA)^2}}&   &     &\uTo>{q_{PA,A}}\cr 
PA&                    &\rTo_{1_{PA}}&                      &PA&\rTo_{(\sigma_{A},1_{PA})}&TPA&\cr
\end{diagram}
from this we can conclude that the diagram
\begin{diagram}[PostScript=dvips]
T^3&&\rTo^{\fst_{T^3A}}&&PT^2A\cr
\uTo<{T\delta_A}&&&\ruTo~{P\delta_A}\cr
T^2A&\rTo~{\fst_{T^2A}}&PTA&&\dTo>{P\snd_{T^2A}}\cr
&&\dTo<{(\sigma_{TA},1_{PTA})}&\rdTo~{1_{PTA}}\cr
\dTo<{\delta_{TA}}&&TPTA&\rTo_{\snd_{TPTA}}&PTA\cr
&&&\rdTo_{q_{P^2A,PA}}&\uTo>{P\snd_{T^2A}}\cr
T^3A&&\rTo_{\fst_{T^3A}}&&PT^2A\cr
\end{diagram}
commutes. So we know
\[\snd\delta_T\delta = \snd(T\delta)\delta\] and
\[(P\snd)\fst\delta_T\delta = (P\snd)\fst(T\delta)\delta\]
If we can show $(P\fst)\fst\delta_T\delta = (P\fst)\fst(T\delta)\delta$,
then it follows that $\delta_T\delta = (T\delta)\delta$ and we are done.
To see this, observe that the following two diagrams are commutative,
and apply Lemma \ref{commute}. 
\begin{diagram}[PostScript=dvips]
TA&&\rTo^{\delta_A}&&T^2A&\rTo^{T\delta_A}&T^3A\cr
\dTo<{\fst_{TA}}&&&&\dTo~{\fst_{T^2A}}&&\dTo>{\fst_{T^3A}}\cr
&&TPA&\rTo^{q_{PA,A}}&PTA&\rTo_{P\delta_A}&PT^2A\cr
&\ruTo~{(\sigma_A,1_{PA})}&\dTo~{\fst_{TPA}}&\ldTo~{P\fst_{TA}}&&&\dTo>{P\fst_{T^2A}}\cr
PA&\rTo_{\sigma_A}&P^2A&\rTo_{P(\sigma_A,1_{PA})}&PTPA&\rTo_{Pq_{PA,A}}&P^2TA\cr
\end{diagram}
\begin{diagram}[PostScript=dvips]
TPA&\rTo^{q_{PA,A}}&PTA&\rTo^{\sigma_{TA}}&P^2TA\cr
\uTo<{(\sigma_A,1_{PA})}&&&\rdTo~{(\sigma_{TA},1_{PTA})}&\uTo~{\fst_{TPTA}}&\luTo^{P\fst_{T^2A}}\cr
PA&&\uTo~{\fst_{T^2A}}&&TPTA&\rTo_{q_{PTA,TA}}&PT^2A\cr
\uTo<{\fst_{TA}}&&&&&&\uTo>{\fst_{T^3A}}\cr
TA&\rTo_{\delta_A}&T^2A&&\rTo_{\delta_{TA}}&&T^3A\cr
\end{diagram}
\cqed
\end{proof}
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Monoids and Semigroups}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Recall that a monad in a category $\C$ is a triple $(T,\mu,\eta)$
where $T$ is an endofunctor on $\C$, $\mu\colon T^2\to T$, and
$\eta\colon 1_\C \to T$, such that the following diagrams commute:
\begin{diagram}
T^3&\rTo^{\mu_T}&T^2&T&\rTo^{\eta_T}&T^2&\lTo^{T\eta}&T\cr
\dTo<{T\mu}&&\dTo>\mu&&\rdTo<{1_T}&\dTo~{\mu}&\ldTo>{1_T}\cr
T^2&\rTo_\mu&T&&&T\cr
&(i)&&&&(ii)\cr
\end{diagram}
Now a monad, by design, strongly resembles a monoid; The two diagrams
assert that the 'multiplication' $\mu$ looks associative, and that
$\eta$ is a 'unit' on the left and right. In fact if $\C$ is $\Sets$,
and $T$ is $M\times\dash$ for some set $M$, then $(T,\mu,\eta)$ is a monad
if and only $(T1, \mu_1, \eta_1)$ is a monoid. By analogy with the
relationship between the definition semigroup and monoid, we
explore the effect of dropping the requirement that diagram (ii) commutes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The Modal Logic of Noncontingency}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The modal logic $NC$ is axiomatized by beginning with the usual axiomization
of propositional logic, and adding a new symbol `$\nc$', read `it is not contingently the case
that', and two axioms,
\[K: \nc(A\imp B) \imp(\nc A \imp \nc B)\]
\[4: \nc A \imp\nc\nc A\]


\begin{diagram}
T^2A&&&\rTo^{\delta_{TA}}&&&T^3A\cr
&\rdTo~{\gamma_{TA}}&&&&\ruTo~{\alpha_{TA}}\cr
&&(PTA)^2\times TA&\rTo^{\beta_{TA}}&PTA\times T^2A&&\cr
\dTo~{\fst_{T^2A}}&&\dTo~{\fst_{(PTA)^2 \times TA}}&&\dTo~{\fst_{PTA\times T^2A}}&&\dTo~{\fst_{T^3A}}\cr
   &                    &(PTA)^2       &                      &   &   &PT^2A\cr
   &\ruTo~{\Delta_{PTA}}&              &\rdTo~{\fst_{(PTA)^2}}&   &     &\uTo>{q_{PTA,TA}}\cr 
PTA&                    &\rTo_{1_{PTA}}&                      &PTA&\rTo_{(\sigma_{TA},1_{PTA})}&TPTA&\cr
\end{diagram}


\begin{diagram}
T^2A&&&\rTo^{T\delta_A}&&&T^3A\cr
&\rdTo~{T\gamma_A}&&&&\ruTo~{T\alpha_A}&\cr
&&T((PA)^2\times A)&\rTo^{T\beta_A}&T(PA\times TA)&&\cr
\dTo~{\fst_{T^2A}}&&\dTo~{\fst_{T((PA)^2 \times A)}}&&\dTo~{\fst_{T(PA\times TA)}}&&\dTo~{\fst_{T^3A}}\cr
&&P((PA)^2\times A)&\rTo_{P\beta_A}&P(PA\times TA)&&\cr
&\ruTo~{P\gamma_A}&&&&\rdTo~{P\alpha_A}\cr
PTA&&&\rTo_{P\delta_A}&&&PT^2A\cr
\end{diagram}