HuJ

draft/draft.tex

@@ -2184,6 +2184,8 @@ $\sigma$ is defined as below:
 	\end{cases}
 \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;(FR)^\dagger;\appr=\powf X\times \powf X$, so $R\subseteq \appr;(FR)^\dagger;\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.
 \end{example}
 \subsection{The concrete proof}
 %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}