more

draft/draft.tex

@@ -676,7 +676,14 @@ Now, we prove $Sg(\mu') = \nu$.
 \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, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$.
 \end{definition}
-
+%
+%\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 existing in both categories $\rel(\BC)$ and $\spa(\BC)$, there is 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)$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel(\BC)$.
+%\end{prop}
+%\begin{proof}
+%	Trivial by the definitions.\qed
+%\end{proof}
+%
 \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}. The already introduced type of morphisms is onymous. For functions $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, $(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)$ is an anonymous morphism in $\spa$ if:
 \begin{gather*}
@@ -687,7 +694,7 @@ From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$
 	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
 \end{gather*}
 From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to show the categories of spans and relations with onymous morphisms.
-\begin{prop}
+\begin{prop}\label{prop:rel-rela}
 	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 existing in both categories $\rel$ and $\rel_a$, there is a 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_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
@@ -703,7 +710,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 	$(\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}
+\begin{prop}\label{prop:spa-spaa}
 	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 existing in both categories $\spa$ and $\spa_a$, there is a 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_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
@@ -712,7 +719,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 	($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed
 \end{proof}
 
-\begin{prop}
+\begin{prop}\label{prop:rela-spaa}
 	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 existing in both categories $\rel_a$ and $\spa_a$, there is a 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_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
 \end{prop}
 \begin{proof}
@@ -721,7 +728,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re
 	($\Leftarrow$): As $\rel_a$ is a subcategory of $\spa_a$, this is trivial.\qed
 \end{proof}
 
-\begin{prop}
+\begin{prop}\label{prop:rel-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 existing in both categories $\rel$ and $\spa$, there is 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$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$.
 \end{prop}
 \begin{proof}
@@ -996,8 +1003,40 @@ The given definition is highly abstract. There is a relation lifting that abstra
 \begin{definition}[Hermida-Jacobs Bisimulation]
 	In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.   
 \end{definition}
+%
+\begin{prop}
+	In a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation. 
+\end{prop}
+\begin{proof}
+	\todo{Finish.}
+\end{proof}
+%
 \subsection{Coalgebraic Bisimulation in Set}
-The have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$.
+We have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$, respectively called \emph{span-based bisimulation} and \emph{relator-based bisimulation}.
+%
+\begin{definition}[Hughes-Jacobs Bisimulation]
+	A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel_a$ is a \emph{Hughes-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, whenever there exists a morhpism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.
+\end{definition}
+%
+\begin{definition}[Span-Based Bisimulation]
+	A span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa_a$ is a \emph{span-based bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, whenever there exists a morhpism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.
+\end{definition}
+%
+\begin{prop}
+	In $\Set$, for $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, 
+	\begin{enumerate}
+		\item Assuming the axiom of choice span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation.
+		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation.
+		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	(1): Follows from~\autoref{prop:spa-spaa}.
+	
+	(2): Follows from~\autoref{prop:rel-rela}.
+	
+	(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. 
+\end{proof}
 %
 \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$.