homework in progress

draft/draft.tex

@@ -614,8 +614,7 @@ Now, we prove $Sg(\mu') = \nu$.
 	\end{itemize}\qed
 \end{proof}
 
-
-\section{Coalgebraic Bisimulation}%\label{sec:}
+\section{Spans and Relations}
 In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
 products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
 such spans $(X \stackrel{p_1}{\leftarrow} R
@@ -624,19 +623,19 @@ We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
 A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$
 ($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ 
 in $\BC$ that the following diagram commutes:
-	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
-			{X_1} \& R \& {X_2} \\
-			{Y_1} \& S \& {Y_2}
-			\arrow["{g_1}"', from=1-1, to=2-1]
-			\arrow["{{p_1}}"', from=1-2, to=1-1]
-			\arrow["{{p_2}}", from=1-2, to=1-3]
-			\arrow["f", from=1-2, to=2-2]
-			\arrow["{g_2}", from=1-3, to=2-3]
-			\arrow["{q_1}", from=2-2, to=2-1]
-			\arrow["{q_2}"', from=2-2, to=2-3]
-		\end{tikzcd}
-	\end{equation*}
+\begin{equation*}
+	\begin{tikzcd}[ampersand replacement=\&]
+		{X_1} \& R \& {X_2} \\
+		{Y_1} \& S \& {Y_2}
+		\arrow["{g_1}"', from=1-1, to=2-1]
+		\arrow["{{p_1}}"', from=1-2, to=1-1]
+		\arrow["{{p_2}}", from=1-2, to=1-3]
+		\arrow["f", from=1-2, to=2-2]
+		\arrow["{g_2}", from=1-3, to=2-3]
+		\arrow["{q_1}", from=2-2, to=2-1]
+		\arrow["{q_2}"', from=2-2, to=2-3]
+	\end{tikzcd}
+\end{equation*}
 
 \begin{definition}[Relation Lifting]
 	Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
@@ -657,21 +656,21 @@ by the image factorization in regular categories. \ppnote{Initially, I wanted to
 %
 %\begin{equation*}
 %	\begin{tikzcd}[ampersand replacement=\&]
-%		R \& {R^\dagger} \&\& {X\times X}
-%		\arrow["{e_R}"', two heads, from=1-1, to=1-2]
-%		\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
-%		\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
-%	\end{tikzcd}
+	%		R \& {R^\dagger} \&\& {X\times X}
+	%		\arrow["{e_R}"', two heads, from=1-1, to=1-2]
+	%		\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
+	%		\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
+	%	\end{tikzcd}
 %\end{equation*}
 We define a functor of type $(-)^\dagger\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:
 
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
-			R \& {R^\dagger} \&\& {X\times Y}
-			\arrow["{e_R}"', two heads, from=1-1, to=1-2]
-			\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
-			\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
-		\end{tikzcd}
+		R \& {R^\dagger} \&\& {X\times Y}
+		\arrow["{e_R}"', two heads, from=1-1, to=1-2]
+		\arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4]
+		\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
+	\end{tikzcd}
 \end{equation*}
 
 So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
@@ -692,7 +691,37 @@ For the time being, we limit the discussion to the case $\BC=\Set$. For simplici
 We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us 
 call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields 
 an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
+\begin{prop}
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\spa$, there is an anonymous morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$ in $\spa$.
+\end{prop}
+\begin{proof}
+	$(\Rightarrow):$ We define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
+	\begin{align*}
+		g_1\comp p_1(x_1,x_2)&\\
+		=&g_1(x_1)\\
+		=&q_1(g(x_1),g(x_2))\\
+		=&q_1\comp w(x_1,x_2)
+	\end{align*}
+	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
 	
+	$(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed
+\end{proof}
+
+\begin{prop}
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\rel$, there is an anonymous morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$ in $\rel$.
+\end{prop}
+\begin{proof}
+	\todo{Finish}
+\end{proof}
+
+\begin{prop}
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\rel$, there is an anonymous morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ iff there is an onymous $(g_1,g_2,w)$ of the same type, with the witness $w\c R\to S$.
+\end{prop}
+\begin{proof}
+	\todo{Finish}
+\end{proof}
+
+\section{Coalgebraic Bisimulation}%\label{sec:}
 By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we 
 can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- 
 \autoref{fig:anonymous_onymous} contains a comprehensible summary.