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

draft/draft.tex

@@ -1876,7 +1876,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 	\end{align*}
 	So, from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$.\qed
 \end{proof}
-First, we define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
+We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
 \begin{gather*}
 	\forall x_1,x_2\in X,\\
 	\sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2).
@@ -1915,7 +1915,7 @@ First, we define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
 %\begin{rem}
 %	Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
 %\end{rem}
-Since $\subseteq$ is a liftable order, we have the following lemma. The liftability is not used in the proof, but $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
+Since $\subseteq$ is a liftable order, we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
 \begin{lemma}\label{lem:alph-prod}
 	Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$. 
 \end{lemma}
@@ -1925,24 +1925,27 @@ Since $\subseteq$ is a liftable order, we have the following lemma. The liftabil
 	\qed
 \end{proof}
 \begin{prop}\label{prop:sym-rel-bisim}
-	Assuming that $R$ is a symmetric relation, $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation:
+	Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation:
 	\begin{gather*}
 		\sigma\join(\powf s\comp\sigma\comp s)
 	\end{gather*}
 \end{prop}
 \begin{proof}
-	For every $(x_1,x_2)\in R$ by~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have 
+	For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have 
 	\begin{gather*}
 		\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
 		\powf p_1\comp\sigma(x_1,x_2),
 	\end{gather*}
-	and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have
+	and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have
 	\begin{gather*}
 		\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
 		\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
 	\end{gather*}
-	Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be a bisimulation.\qed
+	Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed
 \end{proof}
+\begin{cor}
+	Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well.
+\end{cor}
 
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}