diff --git a/draft/draft.tex b/draft/draft.tex index d0966d0..29debd5 100644 --- a/draft/draft.tex +++ b/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.}