minor

draft/draft.tex

@@ -1848,7 +1848,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %\end{proof}
 \subsection{The concrete proof}
 \begin{lemma}\label{lem:sim-opsim-inc}
-	Assuming that $\sigma\c R\to\powf R$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have:
+	Assuming that $\sigma\c R\to\powf R$ is witness for the symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
 		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I}
 		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II}
@@ -1868,7 +1868,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 	\end{align*}
 	So, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we have $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$.
 	
-	Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where 
+	Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where 
 	\begin{align*}
 		\powf p_1\comp\sigma(x_2,x_1)&\\
 		&=\powf p_1\comp\sigma\comp s(x_1,x_2)\\
@@ -1915,7 +1915,7 @@ 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 if $\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 (\autoref{def:liftable-ord}), 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}