homework

draft/draft.tex

@@ -691,8 +691,34 @@ 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.}
+We define the category of spans and relations.
+\begin{definition}[Category of Spans]
+	For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(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)$, whenever 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*}
+\end{definition}
+
+\begin{definition}[Category of Relations]
+	For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is the category that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\spa(\BC)$ if $\brks{p_1,p_2}$ is a monomorphism, then $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ is also an object in $\rel(\BC)$. A morphism $(g_1,g_2,w)\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(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(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(\BC)$ as well.
+\end{definition}
+\todo{See if the comparison that you are doing for $\Set$ can also be done here only for the case of onymous-relation and onymous-span.}
+
+\subsection{Spans and Relations in $\Set$}
+From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. 
+
 \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$.
+	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 in $\spa$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
 	$(\Rightarrow):$ We define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
@@ -708,19 +734,30 @@ an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove
 \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$.
+	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 morhpism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness $w\c R\to S$.
 \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$.
+	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)$ iff $(g_1,g_2)$ is an anonymous morphism of the same type 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 $\spa$, there is an onymous morphism $(g_1,g_2,w)\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 $(g_1,g_2,w)$ is an onymous morphism of the same type in $\rel$.
+\end{prop}
+\begin{proof}
+	\todo{Finish}
+\end{proof}
+\todo{Give the comparison between the category of sets and binary relations with $\rel$ that you defined here!}
+
+\subsection{Categories of Spans and Relations as Double Categories}
+As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an abstract category $\BC$ is replacing $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!].
+\todo{Finish at last. "at last" means after finishing the section for bisimulation without talking about double categories.} 
 \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}) -- 
@@ -875,6 +912,7 @@ We do not know if this definition exists anywhere.
 
 \todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}
 
+
 %
 \section{Coalgebraic Simulation}
 We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.