Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

draft/draft.tex

@@ -687,7 +687,7 @@ Now, we prove $Sg(\mu') = \nu$.
 \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, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$.
+For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. 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}
@@ -708,7 +708,7 @@ From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$
 \end{gather*}
 From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to denote the categories of spans and relations with onymous morphisms.
 \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$.
+	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\sgnote{Unique?} $w\c R\to S$.
 \end{prop}
 \begin{proof}
 	$(\Rightarrow):$ For every $(x_1,x_2)\in R$ we define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
@@ -732,7 +732,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 	($\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}\label{prop:rela-spaa}
+\begin{prop}\label{prop:rela-spaa}\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
 	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}
@@ -771,7 +771,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 
 \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 arbitrary category $\BC$ is replaced with $\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.
-\begin{definition}[(Weak) Double Categories]
+\begin{definition}[(Weak) Double Categories]\sgnote{Add citation.}
 	Given categories $\BC_0$ and $\BC_1$, a double category $\BC_1\rightrightarrows\BC_0$, consists of
 	\begin{itemize}
 		\item a category $\BC_0$ of objects and morphisms,
@@ -1393,13 +1393,13 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 %
 \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 Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$\sgnote{Is it a relation or a general span?} 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
+	$(1)$: Trivial.\sgnote{Does not look so trivial.}\\
+	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\sgnote{Add more details.}\qed
 \end{proof}
 %
 \subsection{Simulations in Set}