some corrections and ednotes

draft/draft.tex

@@ -2192,22 +2192,22 @@ Now, we prove our main statement.
 \end{cor}
 Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
 \subsection{Maybe Functor}
-We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$.\\
+We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_{X+1}\cup\{(\bot,x)\mid x\in X\}$.\\
 Now, we prove that the given order on the maybe functor is a liftable one.
 \begin{lemma}\label{lem:maybe-lif}
 	The order structure on the set-functor $FX=X+1$ is a liftable order.
 \end{lemma}
 \begin{proof}
-	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
+	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr Fg(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $Fg(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
 	\begin{itemize}
-		\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $g+1(k')=\bot=h$.  
+		\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $Fg(k')=\bot=h$.
-		
+
-		\item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed
+		\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}
-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=(p_1+1)\comp\sigma$.
+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)$ 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)$ such that $FX=X+1$, then for every $(x_1,x_2)\in R$ either
 	\begin{gather*}
 		\alpha(x_1),\alpha(x_2)\in X,
 	\end{gather*} 
@@ -2217,17 +2217,17 @@ So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra
 	\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 $p_1+1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in $ we have the following:
+	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.}:
 	\begin{enumerate}
-		\item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
+		\item $\alpha(x_1)=Fp_1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
-		\item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
+		\item $\alpha(x_2)=Fp_1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
-		\item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
+		\item $\alpha(x_1)\sappr Fp_2\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
-		\item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
+		\item $\alpha(x_2)\sappr Fp_2\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
 	\end{enumerate}
 	Now, we have two cases:
 	\begin{itemize}
-		\item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $p_1+1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $p_2+1\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
+		\item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $Fp_1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $Fp_2\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
-		\item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $p_2+1\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $p_1+1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
+		\item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $Fp_2\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $Fp_1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
 	\end{itemize}
 \end{proof}
 %\begin{proof}
@@ -2264,24 +2264,24 @@ So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra
 			(\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X
 		\end{cases}
 	\end{gather*}
-	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.
+	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $Fp_i\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.
-	Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $\alpha(x_i)\in X=(p_i+1)\comp\beta(x_1,x_2)$ we have $\beta(x_1,x_2)\in R$. 
+	Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $Fp_i\comp\beta(x_1,x_2)=\alpha(x_i)\in X$ we have $\beta(x_1,x_2)\in R$.
 	\qed
 \end{proof}
 
-Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.
+Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.\sgnote{This abstract order is coarser than (not the concretisation of) the pointwise Set order at \autoref{lem:set-ord-str}: here the \emph{whole} map must be $\bot$, whereas pointwise a map may be $\bot$ on some points and agree elsewhere. Please check the two agree on the hom-sets you actually use, or justify why the coarser order suffices.}
 %Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one.
 \begin{lemma}\label{lem:maybe-lif-abs}
 	The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
 \end{lemma}
 \begin{proof}
-	For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr g+1\comp k$ that means we have two cases:
+	For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr Fg\comp k$ that means we have two cases:
 	\begin{itemize}
-		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $g+1\comp k'=h$.
+		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $Fg\comp k'=h$.
-		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $g+1\comp k'=h$.\qed
+		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $Fg\comp k'=h$.\qed
 	\end{itemize}
 \end{proof}
-To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. In our case, we take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
+To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. We take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
 \begin{equation*}
 	\begin{tikzcd}[ampersand replacement=\&]
 		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
@@ -2317,7 +2317,8 @@ So, we have the following:
 \begin{gather*}
 	R\iso R_{X^2}+R_{2\times X}+R_{1}
 \end{gather*}
-And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$. 
+And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$.
+\sgnote{This abstraction is unfinished: the crux $R_{2\times X}\iso 0$ (the ``no mixed pairs'' content of \autoref{lem:maybe-func-set}) is stated but not proved, and the subsection ends here. Either complete the argument or mark it clearly as work in progress.}
 \section{Relators}
 \subsection{Two-way similarity in Hughes-Jacobs}
 Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is: