span-based sim

draft/draft.tex

@@ -667,7 +667,7 @@ Now, we prove $Sg(\mu') = \nu$.
 %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]
+\begin{definition}[Category of Spans]\ppnote{Paul Levy said he doesn't like this name for this category as "category of spans" is used for a different category that is a bicategory.}
 	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=\&]
@@ -1002,24 +1002,45 @@ The given definition is highly abstract. There is a relation lifting that abstra
 	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}
+\begin{lemma}\label{lem:morph-spa-rel}
-	For a regular category $\BC$ with the axiom of choice, assuming that in $\rel(\BC)$, there is a morphism $(g_1,g_2,w)$ from an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$, then there exist a morphism $(g_1,g_2,v)$ from $(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 a regular category $\BC$ with the axiom of choice, assuming that $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$ is an object in $\spa(\BC)$, if for an object $A$ in $\BC$ we have a morphism $w\c A\to S^\dagger$, then there exist a morphism $v\c A\to S$ such that for $i\in\{1,2\}$, we have $q_i\comp v=q_i^\dagger\comp w$.
-\end{prop}
+\end{lemma}
 \begin{proof}
 	Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have:
 	\begin{align*}
 		q_i\comp v&\\
 		=&q^\dagger_i\comp e_s\comp v\\
 		=&q^\dagger_i\comp e_s\comp s\comp w\\
-		=&q^\dagger_i\comp w\\
+		=&q^\dagger_i\comp w
-		=&g_i\comp p_i
 	\end{align*}
 	\qed
 \end{proof}
 %
-\begin{cor}\label{cor:HeJ-AM}
+%\begin{prop}
-	For 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. 
+%	For a regular category $\BC$ with the axiom of choice, assuming that in $\rel(\BC)$, there is a morphism $(g_1,g_2,w)$ from an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$, then there exist a morphism $(g_1,g_2,v)$ from $(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)$.
-\end{cor}
+%\end{prop}
+%\begin{proof}
+%	Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have:
+%	\begin{align*}
+%		q_i\comp v&\\
+%		=&q^\dagger_i\comp e_s\comp v\\
+%		=&q^\dagger_i\comp e_s\comp s\comp w\\
+%		=&q^\dagger_i\comp w\\
+%		=&g_i\comp p_i
+%	\end{align*}
+%	\qed
+%\end{proof}
+%
+\begin{prop}\label{prop:HeJ-AM}
+	\begin{enumerate}
+		\item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an AM-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is a HJ-bisimulation.
+		\item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an AM-bisimulation.
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	$(1)$: Trivial.\\
+	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\qed
+\end{proof}
 %
 \subsection{Coalgebraic Bisimulation in Set}
 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{Hughes-Jacobs bisimulation}.
@@ -1048,7 +1069,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	(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$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\qed
 \end{proof}
 \begin{cor}
-	Recalling~\autoref{cor:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
+	Recalling~\autoref{prop:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice.
 \end{cor}
 \begin{figure}[t]
 	\centering
@@ -1068,10 +1089,61 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 \subsection{Bisimulation in Double Categories}
 \todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".}
 %
-\section{Spans and Relations with Lax Morphisms}
+
-\todo{Finish!}
 \section{Coalgebraic Simulation}
 \todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.}
+\begin{definition}[Aczel-Mendler Simulation]
+	Assuming that $\appr$ is a natural order structure on a functor $F\c\BC\to\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\spa(\BC)$ is an \emph{Aczel-Mendler simulation} from a coalgebra $(X,\alpha)$ to $(Y,\beta)$, whenever the following diagram commutes laxly:
+	\begin{equation}\label{eq:diag-am-sim}
+		\begin{tikzcd}[ampersand replacement=\&]
+			X \& R \& Y \\
+			FX \& FR \& FY
+			\arrow["\alpha"', from=1-1, to=2-1]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["\sigma", from=1-2, to=2-2]
+			\arrow["\beta", from=1-3, to=2-3]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
+			\arrow["{{Fp_1}}", from=2-2, to=2-1]
+			\arrow["{{Fp_2}}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation}
+\end{definition}
+%
+\begin{definition}[Hermida-Jacobs Simulation]
+	Assuming that $\appr$ is a natural order structure on a functor $F\c\BC\to\BC$, an $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\rel(\BC)$ is a \emph{Hermida-Jacobs simulation} from a coalgebra $(X,\alpha)$ to $(Y,\beta)$, whenever the following diagram commutes laxly:
+	\begin{equation}\label{eq:diag-hj-sim}
+		\begin{tikzcd}[ampersand replacement=\&]
+			X \& R \& Y \\
+			FX \& (FR)^\dagger \& FY
+			\arrow["\alpha"', from=1-1, to=2-1]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
+			\arrow["{p_1}"', from=1-2, to=1-1]
+			\arrow["{p_2}", from=1-2, to=1-3]
+			\arrow["\sigma", from=1-2, to=2-2]
+			\arrow["\beta", from=1-3, to=2-3]
+			\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
+			\arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1]
+			\arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3]
+		\end{tikzcd}
+	\end{equation}
+\end{definition}
+%
+\begin{prop}
+	\begin{enumerate}
+		\item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an AM-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is a HJ-simulation.
+		\item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an AM-simulation.
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	$(1)$: Trivial.\\
+	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\qed
+\end{proof}
+%
+\subsection{Simulations in Set}
+
+
 %We show the category of partially ordered sets with monotone functions between them with $\poset$. 
 %\begin{definition}[A Partial Order Over a Functor]
 %	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes: