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

draft/draft.tex

@@ -311,7 +311,7 @@
 		}%
 	}%
 }
-\newcommand{\sub}{\mathcal{S}}
+\newcommand{\sub}{\mathcal{D}_{\leq1}}
 
 
 \newcommand{\bba}{
@@ -745,7 +745,8 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 \end{proof}
 %
 \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 of 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 unique witness $w\c R\to S$.
+Let $(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)$
+be jointly-monic spans. Then 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 unique witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
 %	$(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have:
@@ -835,7 +836,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10]  (m-2-2);
 %		
 	\end{tikzpicture}
-	\caption{Summery of results in this section about when we have a morphism in the source of an arrow then we have a morphism in the target in $\Set$.}
+	\caption{Summary of results in this section about when we have a morphism in the source of an arrow then we have a morphism in the target in $\Set$.}
 	\label{fig:morph-summery}
 \end{figure}
 %\begin{notation}
@@ -1642,7 +1643,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 		\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
 		
 	\end{tikzpicture}
-	\caption{Summery of results in this section about notions of simulation in $\Set$.}
+	\caption{Summary of results in this section about notions of simulation in $\Set$.}
 	\label{fig:sim-summery}
 \end{figure}
 %\begin{center}
@@ -1756,7 +1757,8 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 	They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
 \end{proof}
 \begin{cor}
-	Assuming that the order structure $\appr$ on a functor $F\c\Set\to\Set$ is liftable and coliftable, all the notions of simulation given by relators mentioned in~\autoref{ex:lax-rels}.
+	Assuming that the order structure $\appr$ on a functor $F\c\Set\to\Set$ is liftable and coliftable, all the notions of simulation given by relators mentioned in~\autoref{ex:lax-rels}
+	are equivalent.
 \end{cor}
 %
 \begin{prop}\label{prop:HeJ-HuJ}