diff --git a/draft/draft.tex b/draft/draft.tex index 9ecfd4a..42cc597 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1001,13 +1001,25 @@ The given definition is highly abstract. There is a relation lifting that abstra In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$. \end{definition} % -\begin{prop}\label{prop:HeJ-AM} - In a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation. +\begin{prop} + For a regular category $\BC$ with the axiom of choice, assuming that in $\rel(\BC)$, there is a morphism $(g_1,g_2,w)$ from an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$, then there exist a morphism $(g_1,g_2,v)$ from $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$. \end{prop} \begin{proof} - \todo{Finish.} + Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have: + \begin{align*} + q_i\comp v&\\ + =&q^\dagger_i\comp e_s\comp v\\ + =&q^\dagger_i\comp e_s\comp s\comp w\\ + =&q^\dagger_i\comp w\\ + =&g_i\comp p_i + \end{align*} + \qed \end{proof} % +\begin{cor}\label{cor:HeJ-AM} + For a regular category $\BC$ with the axiom of choice, every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is an Aczel-Mendler bisimulation. +\end{cor} +% \subsection{Coalgebraic Bisimulation in Set} We have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$, respectively called \emph{span-based bisimulation} and \emph{relator-based bisimulation}. % @@ -1035,7 +1047,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi (3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\qed \end{proof} \begin{cor} - Recalling~\autoref{prop:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice. + Recalling~\autoref{cor:HeJ-AM}, all the four introduced definitions for bisimulation (\autoref{fig:anonymous_onymous}) are equivalent under the axiom of choice. \end{cor} \begin{figure}[t] \centering @@ -2513,20 +2525,22 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined \end{cases}\qquad \begin{tikzpicture}[scale=0.1] \tikzstyle{every node}+=[inner sep=0pt] - \draw [black] (23.8,-25.2) circle (3); - \draw (23.8,-25.2) node {$1$}; - \draw [black] (42.4,-25.2) circle (3); - \draw (42.4,-25.2) node {$2$}; - \draw [black] (33,-34.6) circle (3); - \draw (33,-34.6) node {$3$}; - \draw [black] (22.477,-22.52) arc (234:-54:2.25); - \fill [black] (25.12,-22.52) -- (26,-22.17) -- (25.19,-21.58); - \draw [black] (41.077,-22.52) arc (234:-54:2.25); - \fill [black] (43.72,-22.52) -- (44.6,-22.17) -- (43.79,-21.58); - \draw [black] (26.8,-25.2) -- (39.4,-25.2); - \fill [black] (39.4,-25.2) -- (38.6,-24.7) -- (38.6,-25.7); - \draw [black] (40.28,-27.32) -- (35.12,-32.48); - \fill [black] (35.12,-32.48) -- (36.04,-32.27) -- (35.33,-31.56); + \draw [black] (25.6,-20.9) circle (3); + \draw (25.6,-20.9) node {$1$}; + \draw [black] (44.9,-20.9) circle (3); + \draw (44.9,-20.9) node {$2$}; + \draw [black] (34.5,-32) circle (3); + \draw (34.5,-32) node {$3$}; + \draw [black] (24.277,-18.22) arc (234:-54:2.25); + \fill [black] (26.92,-18.22) -- (27.8,-17.87) -- (26.99,-17.28); + \draw [black] (43.577,-18.22) arc (234:-54:2.25); + \fill [black] (46.22,-18.22) -- (47.1,-17.87) -- (46.29,-17.28); + \draw [black] (33.177,-29.32) arc (234:-54:2.25); + \fill [black] (35.82,-29.32) -- (36.7,-28.97) -- (35.89,-28.38); + \draw [black] (42.85,-23.09) -- (36.55,-29.81); + \fill [black] (36.55,-29.81) -- (37.46,-29.57) -- (36.73,-28.89); + \draw [black] (28.6,-20.9) -- (41.9,-20.9); + \fill [black] (41.9,-20.9) -- (41.1,-20.4) -- (41.1,-21.4); \end{tikzpicture} \end{gather*} $\sigma$ is defined as below: @@ -2539,9 +2553,9 @@ This counter-example also works as a counter-example for Hughes-Jacobs definitio 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 +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\})\}. + \forall w\in R,\quad\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} @@ -2555,12 +2569,12 @@ Indeed, $\sigma^\dagger$ is a witness for $R$ to be an HJ-simulation, but it is \begin{gather*} \forall w\in R,\quad\sigma(w)=\{(1,1),(2,1),(3,1)\} \end{gather*} - Additionally we define $\sigma^\dagger$ as follows as a witness for $R$ to be an HJ-simulation: + Additionally, we define $\sigma^\dagger$ as follows as a witness for $R$ to be an HJ-simulation: \begin{gather*} - \sigma^\dagger(w)=\{(\{1,2,3\},\{1\})\} + \forall w\in R,\quad\sigma^\dagger(w)=(\{1,2,3\},\{1\}) \end{gather*} - Although $R$ is not an AM-bisimulation not an HJ-bisimulation. -\end{example} + However, $R$ is not an AM-bisimulation nor an HJ-bisimulation regardless of the choice for the order structure. +\end{example} \subsection{From Symmetric Simulation To Bisimulation (Aczel-Mendler)} %\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}