counter-example revisited

draft/draft.tex

@@ -1449,6 +1449,35 @@ We show this relation with $F_\rel(R,X)$.
 	As the mentioned property is equivalent with $\sigma$ being a bisimulation, and bisimulation is unique, then $\sigma_1=\sigma_2$.
 \end{proof}
 %
+\begin{prop}
+	Assuming that the ordering on the functor $F$ is natural, and gives posets, given witness $\sigma$ for a symmetric object $R$ to be an HJ-simulation, if $(Fs)^\dagger\comp\sigma=\sigma\comp s$, then $\sigma$ is a witness for $R$ to be an $HJ$-bisimulation. 
+\end{prop}
+\begin{proof}
+	Since $\sigma$ is a witness that $R$ is an $HJ$-simulation we have
+	\begin{gather*}
+		\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma,\\
+		(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2.
+	\end{gather*}
+	So, we have:
+	\begin{align*}
+		\alpha\comp p_1\appr (Fp_1)^\dagger\comp\sigma&\\
+		\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp\sigma\comp s&\by{naturality of $\appr$}\\
+		\Rightarrow&\alpha\comp p_1\comp s\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&\alpha\comp p_2\appr (Fp_1)^\dagger\comp (Fs)^\dagger\comp\sigma&\by{assumption}\\
+		\Rightarrow&\alpha\comp p_2\appr (Fp_2)^\dagger\comp\sigma&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&\alpha\comp p_2= (Fp_2)^\dagger\comp\sigma&\by{anti symmetry of $\appr$}
+	\end{align*}
+	Similarly we have:
+	\begin{align*}
+		(Fp_2)^\dagger\comp\sigma\appr\alpha\comp p_2&\\
+		\Rightarrow&(Fp_2)^\dagger\comp\sigma\comp s\appr\alpha\comp p_2\comp s&\by{naturality of $\appr$}\\
+		\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_2\comp s&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&(Fp_2)^\dagger\comp(Fs)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{assumption}\\
+		\Rightarrow&(Fp_1)^\dagger\comp\sigma\appr\alpha\comp p_1&\by{\eqref{eq:diag-sym-rel}}\\
+		\Rightarrow&(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1&\by{anti symmetry of $\appr$}
+	\end{align*}\qed
+\end{proof}
+%
 Now, we give a counter example of a symmetric relation on $\Set$ that is a simulation according to~\autoref{def:sim}, i.e, exists the morphism $\sigma$ that commutes laxly in~\eqref{eq:diag-lax-sim}, but $\sigma$ is not a coalgebraic bisimulation, although the relation that we give is clearly a bisimulation in the classic sense. 
 We set $R=\{(A,B),(B,A),(C_1,C_2),(C_2,C_1),(C'_2,C_2),(C_2,C'_2),(C_2,C_2)\}$, $F=\mathbf{Id}$, $\appr=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions:
 \begin{gather*}
@@ -2162,7 +2191,7 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %	\end{gather*}
 %	We have $(Fp_1)^\dagger\comp\sigma$.
 %\end{proof}
-\begin{example}
+\begin{example}\label{ex:sym-sim-bisim-count}
 Assuming that the functor is the powerset endofunctor over the category of sets and injective maps. Let us call this functor $\powfi$. For every $X$, we define the order on $\powfi X$ as $A\appr B$ whenever $|A|\leq |B|$, where $|A|$ and $|B|$ are just cardinalities of $|A|$ and $|B|$ respectively. This is a preorder. Then we define the order over every $\Hom(X,\powfi Y)$ pointwise. We have chosen the category of sets with injective maps because we could not define a functor from $\Set$ to $\preord$ with the mentioned ordering.\\
 We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below:
 \begin{gather*}
@@ -2192,19 +2221,26 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined
 \end{gather*}
 $\sigma$ is defined as below:
 \begin{gather*}
-	\sigma(w)=
-	\begin{cases} 
-		\{(1,2),(2,2)\} & w=(1,2)  \\
-		\{(2,1),(2,2)\} & w=(2,1)  \\
-		\{(1,2),(2,1)\} & w=(1,1)  \\
-		\{(2,2),(1,1)\} & w=(2,2)
-	\end{cases}
+	\sigma(w)=\{(1,2),(2,1)\}
 \end{gather*}
 $R$ is symmetric, and $\sigma$ is a witness for $R$ to be an AM-simulation, but $R$ is not a bisimulation in the traditional sense because $(2,1)\in R$, and $2\to 3$, but $(3,1)$ or $(3,2)$ are not in $R$. It is easy to see that it is not an AM-bisimulation as well because we can not define a function that can serve as an evidence for it as $3$ does not appear in any pair in $R$, while it exists in $\alpha(2)$.
 
 This counter-example also works as a counter-example for Hughes-Jacobs definition of simulation. Actually, $\appr\comp(FR)^\dagger\comp\appr=\powf X\times \powf X$, so $R\subseteq( \appr\comp(FR)^\dagger\comp\appr)$ that means that $R$ is a simulation. Worth noting that they claim that their setting works for an arbitrary category. So, unlike their definition, in the context of the relator-based definitions that only work in $\Set$, this counter-example does not live.
 
 The mentioned ordering is not liftable. Assuming $h\in\Hom(\nats,\powfi \nats)$, $g\c \nats\to \nats$, and $k\in\Hom(\nats,\powfi \nats)$, and they are defined for every $n$ in $\nats$ as $h(n)=\{2\times n\}$, $g(n)=3\times n$, and $k(n)=\{n\}$, then $|h(n)|=|\powfi g(k(n))|=1$ that means $h\appr\powfi g\comp k$ is satisfied, but there is no $k'$ that $h=\powfi g\comp k$ because we can never have $h(1)=\powfi g\comp k'(1)$, as assuming $k'(1)=\{n\}$, and $n$ must be a natural number, then we should have $2=3\times n$ that is impossible.
+
+It is the same for HJ-simulation and HJ-bisimulation. We define $\sigma^\dagger\c R\to (\powf R)^\dagger$ as 
+\begin{gather*}
+	\sigma^\dagger(w)=\{(\{1,2\},\{1,2\})\}.
+\end{gather*}
+Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is not a witness for $R$ to be an HJ-bisimulation. Similar to the case for AM-bisimulation, we can not have a witness for $R$ to be an HJ-bisimulation.
+\end{example}
+
+\begin{example}
+	In~\autoref{ex:sym-sim-bisim-count} we gave a counter-example with an ordering that gives preorders. Now, we slightly change the ordering so that it gives posets. We define $\appr$ as follows:
+	\begin{gather*}
+		A\appr B \iff
+	\end{gather*}
 \end{example}
 
 \subsection{The concrete proof}