diff --git a/draft/draft.tex b/draft/draft.tex index 6b894f5..76c436c 100644 --- a/draft/draft.tex +++ b/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$.