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

draft/draft.tex

@@ -2205,16 +2205,16 @@ Now, we prove that the given order on the maybe functor is a liftable one.
 		\item $h\in Y$: Since $h\appr Fg(k)$ and $h\neq\bot$, we have $h=Fg(k)$. In this case we take $k'=k$, so $k'\appr k$ and $Fg(k')=h$.\qed
 	\end{itemize}
 \end{proof}
+\begin{remark}
+	The mentioned order on the maybe functor is not coliftable.
+\end{remark}
 So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=Fp_1\comp\sigma$.
 \begin{lemma}\label{lem:maybe-func-set}
-	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ such that $FX=X+1$, then for every $(x_1,x_2)\in R$ either
+	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ 
 	\begin{gather*}
-		\alpha(x_1),\alpha(x_2)\in X,
+		\alpha(x_1)\in X\Rightarrow \alpha(x_2)\in X\\
+		\alpha(x_1)=\bot \Rightarrow \alpha(x_2)=\bot
 	\end{gather*} 
-	or
-	\begin{gather*}
-		\alpha(x_1)=\alpha(x_2)=\bot.
-	\end{gather*}
 \end{lemma}
 \begin{proof}
 	By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $Fp_1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in R$ we have the following\sgnote{Consider noting which facts come from the pair $(x_1,x_2)$ (namely \eqref{eq:maybe-func-set-1} and \eqref{eq:maybe-func-set-4}) and which from $(x_2,x_1)$ (namely \eqref{eq:maybe-func-set-2} and \eqref{eq:maybe-func-set-3}); it saves the reader from reconstructing it.}: