From 189005178294af000fb22e5cd68153187d2a49e6 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 10 Aug 2026 18:46:50 +0100 Subject: [PATCH] rel and span comparison --- draft/draft.tex | 1007 ++++++++++++++++++++++++----------------------- 1 file changed, 511 insertions(+), 496 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 5f59634..b8c2049 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -295,6 +295,7 @@ \newcommand{\powfi}{\mathcal{P}_{\mathsf{inj}}} \newcommand{\sappr}{\sqsupseteq} \newcommand{\Dom}{\mathsf{Dom}} +\newcommand{\im}{\mathsf{Im}} \newcommand{\simeet}{% \mathbin{% @@ -626,27 +627,115 @@ Now, we prove $Sg(\mu') = \nu$. \end{proof} \section{Spans and Relations} -In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has -products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ -such spans $(X \stackrel{p_1}{\leftarrow} R -\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono. -We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$. -A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$ -($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ -in $\BC$ that the following diagram commutes: -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {X_1} \& R \& {X_2} \\ - {Y_1} \& S \& {Y_2} - \arrow["{g_1}"', from=1-1, to=2-1] - \arrow["{{p_1}}"', from=1-2, to=1-1] - \arrow["{{p_2}}", from=1-2, to=1-3] - \arrow["f", from=1-2, to=2-2] - \arrow["{g_2}", from=1-3, to=2-3] - \arrow["{q_1}", from=2-2, to=2-1] - \arrow["{q_2}"', from=2-2, to=2-3] - \end{tikzcd} -\end{equation*} +%In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has +%products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\ +%such spans $(X \stackrel{p_1}{\leftarrow} R +%\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono. +%We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$. +%A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$ +%($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ +%in $\BC$ that the following diagram commutes: +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {X_1} \& R \& {X_2} \\ +% {Y_1} \& S \& {Y_2} +% \arrow["{g_1}"', from=1-1, to=2-1] +% \arrow["{{p_1}}"', from=1-2, to=1-1] +% \arrow["{{p_2}}", from=1-2, to=1-3] +% \arrow["f", from=1-2, to=2-2] +% \arrow["{g_2}", from=1-3, to=2-3] +% \arrow["{q_1}", from=2-2, to=2-1] +% \arrow["{q_2}"', from=2-2, to=2-3] +% \end{tikzcd} +%\end{equation*} +% +%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. +%For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly. +% +%We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us +%call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields +%an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.} +%We define the category of spans and relations. +\begin{definition}[Category of Spans] + For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(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)$, whenever the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {X_1} \& R \& {X_2} \\ + {Y_1} \& S \& {Y_2} + \arrow["{g_1}"', from=1-1, to=2-1] + \arrow["{{p_1}}"', from=1-2, to=1-1] + \arrow["{{p_2}}", from=1-2, to=1-3] + \arrow["f", from=1-2, to=2-2] + \arrow["{g_2}", from=1-3, to=2-3] + \arrow["{q_1}", from=2-2, to=2-1] + \arrow["{q_2}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} +\end{definition} + +\begin{definition}[Category of Relations] + For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is the category that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\spa(\BC)$ if $\brks{p_1,p_2}$ is a monomorphism, then $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ is also an object in $\rel(\BC)$. A morphism $(g_1,g_2,w)\c(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)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$. +\end{definition} + +\subsection{Spans and Relations in $\Set$} +From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. The already introduced type of morphisms is onymous. For functions $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, $(g_1,g_2)\c(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)$ is an anonymous morphism in $\spa$ if: +\begin{gather*} + u\in R\Rightarrow \exists v\in S, q_1(v)= g_1\comp p_1(u) \quad\&\quad q_2(v)=g_2\comp p_2(u) +\end{gather*} + In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that forces the elements of relations to be pairs and the existential quantifier refers to a unique element: +\begin{gather*} + (x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S +\end{gather*} +From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to show the categories of spans and relations with onymous morphisms. +\begin{prop} + Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(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)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness $w\c R\to S$. +\end{prop} +\begin{proof} + $(\Rightarrow):$ For every $(x_1,x_2)\in R$ we define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have: + \begin{align*} + g_1\comp p_1(x_1,x_2)&\\ + =&g_1(x_1)\\ + =&q_1(g(x_1),g(x_2))\\ + =&q_1\comp w(x_1,x_2) + \end{align*} + Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$. + + $(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed +\end{proof} + +\begin{prop} + Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(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)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$. +\end{prop} +\begin{proof} + ($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we show with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$. + + ($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed +\end{proof} + +\begin{prop} + Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(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)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$. +\end{prop} +\begin{proof} + ($\Rightarrow$): Assuming that $(g_1,g_2)$ is a morphism in $\spa_a$, then for $(x_1,x_2)\in R$ there exists $v\in S$, such that $q_1(v)=g_1(x_1)$ and $q_2(v)=g_2(x_2)$. Since $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)\in\rel_a$ then the $v$ is unique and $v=(g_1(x_1),g_2(x_2))$. + + ($\Leftarrow$): As $\rel_a$ is a subcategory of $\spa_a$, this is trivial.\qed +\end{proof} + +\begin{prop} + Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\spa$, there is a morphism $(g_1,g_2,w)\c(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)$ in $\spa$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$. +\end{prop} +\begin{proof} + Trivial by the definitions.\qed +\end{proof} + +%\begin{notation} +% In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$. +%\end{notation} + +\subsection{Categories of Spans and Relations as Double Categories} +As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an abstract category $\BC$ is replacing $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!]. +\todo{Finish at last. "at last" means after finishing the section for bisimulation without talking about double categories.} +\section{Coalgebraic Bisimulation}%\label{sec:} \begin{definition}[Relation Lifting] Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes: @@ -695,81 +784,7 @@ So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] \end{tikzcd} \end{equation*} -% -%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. -For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly. - -We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us -call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields -an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.} -We define the category of spans and relations. -\begin{definition}[Category of Spans] - For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(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)$, whenever the following diagram commutes: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {X_1} \& R \& {X_2} \\ - {Y_1} \& S \& {Y_2} - \arrow["{g_1}"', from=1-1, to=2-1] - \arrow["{{p_1}}"', from=1-2, to=1-1] - \arrow["{{p_2}}", from=1-2, to=1-3] - \arrow["f", from=1-2, to=2-2] - \arrow["{g_2}", from=1-3, to=2-3] - \arrow["{q_1}", from=2-2, to=2-1] - \arrow["{q_2}"', from=2-2, to=2-3] - \end{tikzcd} - \end{equation*} -\end{definition} - -\begin{definition}[Category of Relations] - For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is the category that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\spa(\BC)$ if $\brks{p_1,p_2}$ is a monomorphism, then $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ is also an object in $\rel(\BC)$. A morphism $(g_1,g_2,w)\c(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)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well. -\end{definition} -\todo{See if the comparison that you are doing for $\Set$ can also be done here only for the case of onymous-relation and onymous-span.} - -\subsection{Spans and Relations in $\Set$} -From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. - -\begin{prop} - Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\spa$, there is an anonymous morphism $(g_1,g_2)\c(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)$ in $\spa$ iff there is an onymous $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$. -\end{prop} -\begin{proof} - $(\Rightarrow):$ We define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have: - \begin{align*} - g_1\comp p_1(x_1,x_2)&\\ - =&g_1(x_1)\\ - =&q_1(g(x_1),g(x_2))\\ - =&q_1\comp w(x_1,x_2) - \end{align*} - Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$. - - $(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed -\end{proof} - -\begin{prop} - Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\rel$, there is an anonymous morphism $(g_1,g_2)\c(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)$ in $\rel$ iff there is an onymous morhpism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness $w\c R\to S$. -\end{prop} -\begin{proof} - \todo{Finish} -\end{proof} - -\begin{prop} - Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\spa$, there is an anonymous morphism $(g_1,g_2)\c(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)$ iff $(g_1,g_2)$ is an anonymous morphism of the same type in $\rel$. -\end{prop} -\begin{proof} - \todo{Finish} -\end{proof} - -\begin{prop} - Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects in $\spa$, there is an onymous morphism $(g_1,g_2,w)\c(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)$ iff $(g_1,g_2,w)$ is an onymous morphism of the same type in $\rel$. -\end{prop} -\begin{proof} - \todo{Finish} -\end{proof} -\todo{Give the comparison between the category of sets and binary relations with $\rel$ that you defined here!} - -\subsection{Categories of Spans and Relations as Double Categories} -As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an abstract category $\BC$ is replacing $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!]. -\todo{Finish at last. "at last" means after finishing the section for bisimulation without talking about double categories.} -\section{Coalgebraic Bisimulation}%\label{sec:} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- \autoref{fig:anonymous_onymous} contains a comprehensible summary. @@ -940,58 +955,58 @@ We show the category of preorders with monotone functions between them with $\pr \end{equation*} \end{definition} % - -We gave an introduction to Hughes and Jacobs paper. They also have a way to represent simulation relations. In the following, we try to find a suitable formalization for simulation relations, inspired by Hughes and Jacobs. -\subsection{Relations as \cancel{Pullbacks} Spans(?)} -We can not show every relation by pullbacks, but we can just show relations of the form -\begin{gather*} - \{(a,b)\mid f(a)=g(b)\} -\end{gather*} -for some functions $f$ and $g$, when we are in $\Set$, so we can not show every object in $\rel$ using this approach, including $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ that is the target of simulation. Although we can show $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ as a span. - -Assuming, we have a category $\BC$, an object of the category of spans over $\BC$ is $(R,X_1,X_2,p_1,p_2)$ in the form of the following diagram: -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - \& R \\ - {X_1} \&\& {X_2} - \arrow["{p_1}"', from=1-2, to=2-1] - \arrow["{p_2}", from=1-2, to=2-3] - \end{tikzcd} -\end{equation*} -A morhpism from a span $(R,X_1,X_2,p_1,p_2)$ to a span $(S,Y_1,Y_2,q_1,q_2)$ is a morphism $f\c R\to S$ in $\BC$, for which exist $f_1\c X_1\to Y_i$ and $f_2\c X_2\to Y_j$, where $i,j\in\{1,2\}$ and $i\neq j$, and they are in $\BC$, that take part in the following commuting diagram: -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {X_2} \& R \& {X_1} \\ - {Y_j} \& S \& {Y_i} - \arrow["{f_2}"', from=1-1, to=2-1] - \arrow["{p_2}"', from=1-2, to=1-1] - \arrow["{p_1}", from=1-2, to=1-3] - \arrow["f", from=1-2, to=2-2] - \arrow["{f_1}", from=1-3, to=2-3] - \arrow["{q_j}", from=2-2, to=2-1] - \arrow["{q_i}"', from=2-2, to=2-3] - \end{tikzcd} -\end{equation*} -We define a $F$-simulation as the coalgebra of the object $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ that has the following structure in $\BC$: -\begin{tikzcd}[ampersand replacement=\&] - {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \\ - \& FR \& {FX_1} \\ - {\appr_{X_2}} \& {FX_2} \\ - {FX_2} - \arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2] - \arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2] - \arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3] - \arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] - \arrow["{{{{{{{i^1_1}}}}}}}", from=1-3, to=1-4] - \arrow["{{{{{{{i^1_2}}}}}}}", from=1-3, to=2-3] - \arrow["{{{{{{{Fp_1}}}}}}}", from=2-2, to=2-3] - \arrow["{{{{{{{Fp_2}}}}}}}"', from=2-2, to=3-2] - \arrow["{{{{{{{i^2_1}}}}}}}"', from=3-1, to=3-2] - \arrow["{{{{{{{i^2_2}}}}}}}"', from=3-1, to=4-1] -\end{tikzcd} - +% +%We gave an introduction to Hughes and Jacobs paper. They also have a way to represent simulation relations. In the following, we try to find a suitable formalization for simulation relations, inspired by Hughes and Jacobs. +%\subsection{Relations as \cancel{Pullbacks} Spans(?)} +%We can not show every relation by pullbacks, but we can just show relations of the form +%\begin{gather*} +% \{(a,b)\mid f(a)=g(b)\} +%\end{gather*} +%for some functions $f$ and $g$, when we are in $\Set$, so we can not show every object in $\rel$ using this approach, including $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ that is the target of simulation. Although we can show $\rel_\appr(F)(R)\appr_{X_2};\rel(F)(R);\appr_{X_1}$ as a span. +% +%Assuming, we have a category $\BC$, an object of the category of spans over $\BC$ is $(R,X_1,X_2,p_1,p_2)$ in the form of the following diagram: +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% \& R \\ +% {X_1} \&\& {X_2} +% \arrow["{p_1}"', from=1-2, to=2-1] +% \arrow["{p_2}", from=1-2, to=2-3] +% \end{tikzcd} +%\end{equation*} +%A morhpism from a span $(R,X_1,X_2,p_1,p_2)$ to a span $(S,Y_1,Y_2,q_1,q_2)$ is a morphism $f\c R\to S$ in $\BC$, for which exist $f_1\c X_1\to Y_i$ and $f_2\c X_2\to Y_j$, where $i,j\in\{1,2\}$ and $i\neq j$, and they are in $\BC$, that take part in the following commuting diagram: +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {X_2} \& R \& {X_1} \\ +% {Y_j} \& S \& {Y_i} +% \arrow["{f_2}"', from=1-1, to=2-1] +% \arrow["{p_2}"', from=1-2, to=1-1] +% \arrow["{p_1}", from=1-2, to=1-3] +% \arrow["f", from=1-2, to=2-2] +% \arrow["{f_1}", from=1-3, to=2-3] +% \arrow["{q_j}", from=2-2, to=2-1] +% \arrow["{q_i}"', from=2-2, to=2-3] +% \end{tikzcd} +%\end{equation*} +%We define a $F$-simulation as the coalgebra of the object $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ that has the following structure in $\BC$: +%\begin{tikzcd}[ampersand replacement=\&] +% {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \\ +% \& FR \& {FX_1} \\ +% {\appr_{X_2}} \& {FX_2} \\ +% {FX_2} +% \arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2] +% \arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-2] +% \arrow["{{{{{{{\varphi_1}}}}}}}", from=1-2, to=1-3] +% \arrow["{{{{{{{\varphi_2}}}}}}}", from=1-2, to=2-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] +% \arrow["{{{{{{{i^1_1}}}}}}}", from=1-3, to=1-4] +% \arrow["{{{{{{{i^1_2}}}}}}}", from=1-3, to=2-3] +% \arrow["{{{{{{{Fp_1}}}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{{{Fp_2}}}}}}}"', from=2-2, to=3-2] +% \arrow["{{{{{{{i^2_1}}}}}}}"', from=3-1, to=3-2] +% \arrow["{{{{{{{i^2_2}}}}}}}"', from=3-1, to=4-1] +%\end{tikzcd} +% %For $F=B(\mS,-)$ this object has the following structure in $\Set$: %\begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] @@ -1033,356 +1048,356 @@ We define a $F$-simulation as the coalgebra of the object $\appr_{X_1};\rel(F)(R % \end{tikzcd} %\end{equation*} % -We show that if we consider a relation $R$ and its opposite are both simulation relations, then $R$ is a bisimulation. To reach to that goal, we give a formal definition of what we mean by the opposite of $R$ in our categorical setting that we show with $R^\op$. $(R^\op,p'_1,p'_2)$ is a span, that is isomorphic to $R$ via morphism $s\c R\to R^\op$ in $\rel$ that we call swap, and it commutes in the following commutative diagram: -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {X_2} \& R \& {X_1} \\ - {X_2} \& {R^\op} \& {X_1} - \arrow["\id"', from=1-1, to=2-1] - \arrow["{p_2}"', from=1-2, to=1-1] - \arrow["{p_1}", from=1-2, to=1-3] - \arrow["s"', from=1-2, to=2-2] - \arrow["\id", from=1-3, to=2-3] - \arrow["{p'_1}", from=2-2, to=2-1] - \arrow["{p'_2}"', from=2-2, to=2-3] - \end{tikzcd} -\end{equation*} -\begin{lemma} - The relation $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X^\op_2};\rel(F)(R^\op);\appr_{X^\op_1}$. -\end{lemma} -\begin{proof} - We set $s_1\c\appr_{X_1}\to\appr^\op_{X_1}$ and $s_2\c\appr_{X_2}\to\appr^\op_{X_2}$ to be the swaps of $\appr_{X_1}$ and $\appr_{X_2}$, respectively. Since we have - \begin{align*} - i'^{1}_{1}\comp s_1\comp\varphi_1&\\ - &=i^{1}_{2}\comp\varphi_2\\ - &=Fp_1\comp\varphi_2\\ - &=Fp'_2\comp Fs\comp \varphi_2, - \end{align*} - there exists the morphism $s''\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ depicted in the following commutative diagram: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ - FR \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \\ - \& {FR^\op} \& {FX_1} - \arrow["{\varphi_1}", from=1-1, to=1-2] - \arrow["{\varphi_2}"', from=1-1, to=2-1] - \arrow["{s''}", dashed, from=1-1, to=2-2] - \arrow["{s_1}"', from=1-2, to=2-3] - \arrow["Fs"', from=2-1, to=3-2] - \arrow["{{{{{\varphi'_2}}}}}", from=2-2, to=2-3] - \arrow["{{{{{\varphi'_1}}}}}"', from=2-2, to=3-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] - \arrow["{{{{{{{{i'^{1}_1}}}}}}}}"', from=2-3, to=3-3] - \arrow["{{{{{{{{Fp'_2}}}}}}}}", from=3-2, to=3-3] - \end{tikzcd} - \end{equation*} - Similarily, we get $s''^\mone\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ since - \begin{align*} - i^{1}_{2}\comp s_1^\mone\comp\varphi'_2&\\ - &=i'^{1}_{1}\comp\varphi_2'\\ - &=Fp'_2\comp\varphi'_1\\ - &=Fp_1\comp Fs_1^\mone\comp \varphi'_1, - \end{align*} - and it is depicted in the following diagram: - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}} \\ - {FR^\op} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ - \& FR \& {FX_1} - \arrow["{{\varphi'_2}}", from=1-1, to=1-2] - \arrow["{{\varphi'_1}}"', from=1-1, to=2-1] - \arrow["{{s''^\mone}}"', dashed, from=1-1, to=2-2] - \arrow["{s_1^\mone}", from=1-2, to=2-3] - \arrow["{Fs^\mone}"', from=2-1, to=3-2] - \arrow["{{\varphi_1}}", from=2-2, to=2-3] - \arrow["{{\varphi_2}}"', from=2-2, to=3-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] - \arrow["{i_2^1}", from=2-3, to=3-3] - \arrow["{Fp_1}"', from=3-2, to=3-3] - \end{tikzcd} - \end{equation*} - Obviously, $s''$ and $s''^\mone$ are each other's inverse, thus $\appr_{X_1};\rel(F)(R)$ and $\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic. - \begin{align*} - Fp'_1\comp\varphi'_1\comp s''\comp\pi_1&\\ - &=Fp'_1\comp Fs\comp\varphi_2\comp\pi_1\\ - &=Fp_2\comp\varphi_2\comp\pi_1\\ - &=i^2_1\comp\pi_2\\ - &=i'^{2}_{2}\comp s_2\comp \pi_2 - \end{align*} - \begin{tikzcd}[ampersand replacement=\&] - {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ - \& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ - {\appr_{X_2}} \&\& {FR^\op} \\ - \& {\appr_{X_2}^\op} \& {FX_2} - \arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2] - \arrow["{s'}", dashed, from=1-1, to=2-2] - \arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1] - \arrow["{s''}", from=1-2, to=2-3] - \arrow["{{{{{{\pi'_2}}}}}}", from=2-2, to=2-3] - \arrow["{{{{{{\pi'_1}}}}}}"', from=2-2, to=4-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] - \arrow["{\varphi'_1}", from=2-3, to=3-3] - \arrow["{{{s_2}}}", from=3-1, to=4-2] - \arrow["{Fp'_1}", from=3-3, to=4-3] - \arrow["{i'^{2}_{2}}", from=4-2, to=4-3] - \end{tikzcd} - - \begin{align*} - Fp_2\comp\varphi_2\comp s''^\mone\comp\pi'_2&\\ - &=Fp_2\comp Fs^\mone\comp\varphi'_1\comp\pi'_2\\ - &=Fp'_1\comp\varphi'_1\comp\pi'_2\\ - &=i'^{2}_{2}\comp\pi'_1\\ - &=i^{2}_{1}\comp s_2^\mone\comp\pi'_1 - \end{align*} - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \&\& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ - \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ - \&\& FR \\ - {\appr_{X_2}^\op} \& {\appr_{X_2}} \& {FX_2} - \arrow["{{{{{{\pi'_2}}}}}}", from=1-1, to=1-3] - \arrow["{s'^\mone}"', dashed, from=1-1, to=2-2] - \arrow["{{{{{{\pi'_1}}}}}}"', from=1-1, to=4-1] - \arrow["{s''^\mone}", from=1-3, to=2-3] - \arrow["{{{{{{{\pi_1}}}}}}}", from=2-2, to=2-3] - \arrow["{{{{{{{\pi_2}}}}}}}"', from=2-2, to=4-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] - \arrow["{{{{{{{\varphi_2}}}}}}}", from=2-3, to=3-3] - \arrow["{{{{{{{Fp_2}}}}}}}", from=3-3, to=4-3] - \arrow["{{{s_2}^\mone}}"', from=4-1, to=4-2] - \arrow["{{{{{{{i^2_1}}}}}}}"', from=4-2, to=4-3] - \end{tikzcd} - \end{equation*} - So, we could prove that $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ and $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic. $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ by definition, so it is also isomorphic with $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$.\qed - %{\tiny - % \begin{equation*} - % \begin{tikzcd}[ampersand replacement=\&] - % {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \& {FX_1} \\ - % \& {FR^\op} \& {FX_1} \\ - % {\appr_{X_2}^\op} \& {FX_2} \\ - % {FX_2} - % \arrow["{{{{{{\pi'_2}}}}}}"', from=1-1, to=1-2] - % \arrow["{{{{{{\pi'_1}}}}}}", from=1-1, to=3-1] - % \arrow["{{{{\varphi'_2}}}}", from=1-2, to=1-3] - % \arrow[""{name=0, anchor=center, inner sep=0}, "{{{{\varphi'_1}}}}"', from=1-2, to=2-2] - % \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] - % \arrow["{{{{{{{i'^{1}_2}}}}}}}", from=1-3, to=1-4] - % \arrow["{{{{{{{i'^{1}_1}}}}}}}"', from=1-3, to=2-3] - % \arrow["{{{{{{{Fp'_2}}}}}}}", from=2-2, to=2-3] - % \arrow["{{{{{{{Fp'_1}}}}}}}", from=2-2, to=3-2] - % \arrow[""{name=1, anchor=center, inner sep=0}, from=3-1, to=3-2] - % \arrow["{{{{{{{i'^{2}_1}}}}}}}", from=3-1, to=4-1] - % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-1, to=0] - % \arrow["{{{{{{{i'^{2}_2}}}}}}}", from=1, to=3-2] - % \end{tikzcd} - % \end{equation*} - %} -\end{proof} -\begin{prop} - Having $\sigma\c R\to\appr_{X_2};\rel(F)(R);\appr_{X_1}$ and $\sigma^\op\c R^{\op}\to\appr_{X_1};\rel(F)(R^{\op});\appr_{X_2}$ gives rise to a morphism $\gamma\c R\to\rel(F)(R)$, and vice-versa. -\end{prop} -\begin{proof} - {\tiny - \begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - R \&\&\&\& {X_1} \\ - \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \& {X_1} \\ - \&\& FR \& {FX_1} \& {\appr_{X_1}^\op} \\ - \& {\appr_{X_2}} \& {FX_2} \& {FR^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ - {X_2} \& {FX_2} \& {\appr_{X_2}^\op} \&\& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \\ - \& {X_2} \&\&\&\& {R^\op} - \arrow["{{{{{p_1}}}}}", from=1-1, to=1-5] - \arrow["\sigma"', from=1-1, to=2-2] - \arrow["{{{{{p_2}}}}}"', from=1-1, to=5-1] - \arrow["\alpha", from=1-5, to=2-5] - \arrow["{{{{{{\pi_1}}}}}}", from=2-2, to=2-3] - \arrow["{{{{{{\pi_2}}}}}}"', from=2-2, to=4-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] - \arrow["{{{{{{\varphi_1}}}}}}", from=2-3, to=2-4] - \arrow["{{{{{{\varphi_2}}}}}}", from=2-3, to=3-3] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] - \arrow["{{{{{{i^1_1}}}}}}", from=2-4, to=2-5] - \arrow["{{{{{{i^1_2}}}}}}", from=2-4, to=3-4] - \arrow["{{s_1}}", from=2-4, to=3-5] - \arrow["\alpha", from=2-6, to=2-5] - \arrow["{{{{{{Fp_1}}}}}}", from=3-3, to=3-4] - \arrow["{{{{{{Fp_2}}}}}}"', from=3-3, to=4-3] - \arrow["Fs"', from=3-3, to=4-4] - \arrow["{{{{{{i'^{1}_2}}}}}}", from=3-5, to=2-5] - \arrow["{{{{{{i'^{1}_1}}}}}}"', from=3-5, to=3-4] - \arrow["{{{{{{i^2_1}}}}}}"', from=4-2, to=4-3] - \arrow["{{{{{{i^2_2}}}}}}"', from=4-2, to=5-2] - \arrow["{{s_2}}"', from=4-2, to=5-3] - \arrow["{{{{{{Fp'_2}}}}}}", from=4-4, to=3-4] - \arrow["{{{{{{Fp'_1}}}}}}", from=4-4, to=4-3] - \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=225}, draw=none, from=4-5, to=3-4] - \arrow["{{{\varphi'_2}}}", from=4-5, to=3-5] - \arrow[""{name=0, anchor=center, inner sep=0}, "{{{\varphi'_1}}}"', from=4-5, to=4-4] - \arrow["\beta"', from=5-1, to=5-2] - \arrow[""{name=1, anchor=center, inner sep=0}, from=5-3, to=4-3] - \arrow["{{{{{{i'^{2}_1}}}}}}", from=5-3, to=5-2] - \arrow["{{{{{\pi'_2}}}}}"', from=5-5, to=4-5] - \arrow["{{{{{\pi'_1}}}}}", from=5-5, to=5-3] - \arrow["\beta"', from=6-2, to=5-2] - \arrow["{{{{{p'_2}}}}}", from=6-6, to=2-6] - \arrow["{{{{{\sigma^\op}}}}}"', from=6-6, to=5-5] - \arrow["{{{{{p'_1}}}}}"', from=6-6, to=6-2] - \arrow["{{{{{{i'^{2}_2}}}}}}", from=1, to=4-3] - \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=5-5, to=0] - \end{tikzcd} - \end{equation*} - } - ($\Leftarrow$): We assume that we have the morphism $\gamma\c R\to FR$ such that the following diagram commutes: - \begin{equation} - \begin{tikzcd}[ampersand replacement=\&] - {X_2} \& R \& {X_1} \\ - {FX_2} \& FR \& {FX_1} - \arrow["\beta"', from=1-1, to=2-1] - \arrow["{p_2}"', from=1-2, to=1-1] - \arrow["{p_1}", from=1-2, to=1-3] - \arrow["\gamma", from=1-2, to=2-2] - \arrow["\alpha", from=1-3, to=2-3] - \arrow["{Fp_2}", from=2-2, to=2-1] - \arrow["{Fp_1}"', from=2-2, to=2-3] - \end{tikzcd} - \end{equation} - Since $\appr_{X_1}$ and $\appr_{X_1}$ preorders, they each have a morphism $\refl$ that pre-composed with their projections gives identity. As it is depicted in the following diagram the pullback property of ${\appr_{X_1};\rel(F)(R)}$ gives us $\sigma'\c R\to{\appr_{X_1};\rel(F)(R)}$ in the following commutative diagram: - \begin{equation}\label{eq:diag-thm-sig'} - \begin{tikzcd}[ampersand replacement=\&] - R \& {X_1} \& {FX_1} \\ - \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ - \& FR \& {FX_1} - \arrow["{p_1}", from=1-1, to=1-2] - \arrow["{\sigma'}", dashed, from=1-1, to=2-2] - \arrow["\gamma"', bend right=30, from=1-1, to=3-2] - \arrow["\alpha", from=1-2, to=1-3] - \arrow["\refl", from=1-3, to=2-3] - \arrow["{\varphi_1}", from=2-2, to=2-3] - \arrow["{\varphi_2}", from=2-2, to=3-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] - \arrow["{i_2^1}", from=2-3, to=3-3] - \arrow["{Fp_1}"', from=3-2, to=3-3] - \end{tikzcd} - \end{equation} - Then the pullback property of $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ gives us the existence of $\sigma\c R\to \appr_{X_1};\rel(F)(R);\appr_{X_2}$ in the following commutative diagram: - \begin{equation}\label{eq:diag-thm-sig} - \begin{tikzcd}[ampersand replacement=\&] - {X_2} \&\&\& R \\ - \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ - \&\& FR \\ - {FX_2} \& {\appr_{X_2}} \& {FX_2} - \arrow["\beta"', from=1-1, to=4-1] - \arrow["{p_2}"', from=1-4, to=1-1] - \arrow["\sigma"', dashed, from=1-4, to=2-2] - \arrow["{\sigma'}", from=1-4, to=2-3] - \arrow["\gamma", bend left=40, from=1-4, to=3-3] - \arrow["{\pi_1}", from=2-2, to=2-3] - \arrow["{\pi_2}"', from=2-2, to=4-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] - \arrow["{\varphi_2}", from=2-3, to=3-3] - \arrow["{Fp_2}", from=3-3, to=4-3] - \arrow["\refl"', from=4-1, to=4-2] - \arrow["{i_1^2}"', from=4-2, to=4-3] - \end{tikzcd} - \end{equation} - Now, we show that $\sigma$ is a simulation: - \begin{align*} - i^1_1\comp\varphi_1\comp\pi_1\comp\sigma&&\\ - &=i^1_1\comp\varphi_1\comp\sigma'&\by{\eqref{eq:diag-thm-sig}}\\ - &=i^1_1\comp\refl\comp\alpha\comp p_1&\by{\eqref{eq:diag-thm-sig'}}\\ - &=\alpha\comp p_1& - \end{align*} - \begin{align*} - i^2_2\comp\pi_2\comp\sigma&&\\ - &=i^2_2\comp\refl\comp\beta\comp p_2&\by{\eqref{eq:diag-thm-sig}}\\ - &=\beta\comp p_2 - \end{align*} - Considering that $s\c R\to R^\op$ and $s'\c\appr_{X_1};\rel(F)(R);\appr_{X_2}\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are swapping isomorphisms, We set $\sigma^\op\c R^\op\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ to be $\sigma^\op=s'\comp\sigma\comp s^\mone$. Now, we show that $\sigma'$ is a simulation: - \begin{align*} - i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp \sigma^\op&\\ - &=i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp s'\comp\sigma\comp s^\mone\\ - &=i^{1}_{1}\comp\varphi_1\comp\pi_1\comp\sigma\comp s^\mone\\ - &=\alpha\comp p_1\comp s^\mone\\ - &=\alpha\comp p'_2 - \end{align*} - \begin{align*} - i'^{2}_{1}\comp\pi'_1\comp\sigma^\op=&\\ - &=i'^{2}_{1}\comp\pi'_1\comp s'\comp\sigma\comp s^\mone\\ - &=i_2^2\comp\pi_2\comp\sigma\comp s^\mone\\ - &=\beta\comp p_2\comp s^\mone\\ - &=\beta\comp p'_1 - \end{align*} -\end{proof} +%We show that if we consider a relation $R$ and its opposite are both simulation relations, then $R$ is a bisimulation. To reach to that goal, we give a formal definition of what we mean by the opposite of $R$ in our categorical setting that we show with $R^\op$. $(R^\op,p'_1,p'_2)$ is a span, that is isomorphic to $R$ via morphism $s\c R\to R^\op$ in $\rel$ that we call swap, and it commutes in the following commutative diagram: +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {X_2} \& R \& {X_1} \\ +% {X_2} \& {R^\op} \& {X_1} +% \arrow["\id"', from=1-1, to=2-1] +% \arrow["{p_2}"', from=1-2, to=1-1] +% \arrow["{p_1}", from=1-2, to=1-3] +% \arrow["s"', from=1-2, to=2-2] +% \arrow["\id", from=1-3, to=2-3] +% \arrow["{p'_1}", from=2-2, to=2-1] +% \arrow["{p'_2}"', from=2-2, to=2-3] +% \end{tikzcd} +%\end{equation*} +%\begin{lemma} +% The relation $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X^\op_2};\rel(F)(R^\op);\appr_{X^\op_1}$. +%\end{lemma} +%\begin{proof} +% We set $s_1\c\appr_{X_1}\to\appr^\op_{X_1}$ and $s_2\c\appr_{X_2}\to\appr^\op_{X_2}$ to be the swaps of $\appr_{X_1}$ and $\appr_{X_2}$, respectively. Since we have +% \begin{align*} +% i'^{1}_{1}\comp s_1\comp\varphi_1&\\ +% &=i^{1}_{2}\comp\varphi_2\\ +% &=Fp_1\comp\varphi_2\\ +% &=Fp'_2\comp Fs\comp \varphi_2, +% \end{align*} +% there exists the morphism $s''\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ depicted in the following commutative diagram: +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ +% FR \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \\ +% \& {FR^\op} \& {FX_1} +% \arrow["{\varphi_1}", from=1-1, to=1-2] +% \arrow["{\varphi_2}"', from=1-1, to=2-1] +% \arrow["{s''}", dashed, from=1-1, to=2-2] +% \arrow["{s_1}"', from=1-2, to=2-3] +% \arrow["Fs"', from=2-1, to=3-2] +% \arrow["{{{{{\varphi'_2}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{\varphi'_1}}}}}"', from=2-2, to=3-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] +% \arrow["{{{{{{{{i'^{1}_1}}}}}}}}"', from=2-3, to=3-3] +% \arrow["{{{{{{{{Fp'_2}}}}}}}}", from=3-2, to=3-3] +% \end{tikzcd} +% \end{equation*} +% Similarily, we get $s''^\mone\c\appr_{X_1};\rel(F)(R)\to\rel(F)(R^\op);\appr_{X_1}^\op$ since +% \begin{align*} +% i^{1}_{2}\comp s_1^\mone\comp\varphi'_2&\\ +% &=i'^{1}_{1}\comp\varphi_2'\\ +% &=Fp'_2\comp\varphi'_1\\ +% &=Fp_1\comp Fs_1^\mone\comp \varphi'_1, +% \end{align*} +% and it is depicted in the following diagram: +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}} \\ +% {FR^\op} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ +% \& FR \& {FX_1} +% \arrow["{{\varphi'_2}}", from=1-1, to=1-2] +% \arrow["{{\varphi'_1}}"', from=1-1, to=2-1] +% \arrow["{{s''^\mone}}"', dashed, from=1-1, to=2-2] +% \arrow["{s_1^\mone}", from=1-2, to=2-3] +% \arrow["{Fs^\mone}"', from=2-1, to=3-2] +% \arrow["{{\varphi_1}}", from=2-2, to=2-3] +% \arrow["{{\varphi_2}}"', from=2-2, to=3-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] +% \arrow["{i_2^1}", from=2-3, to=3-3] +% \arrow["{Fp_1}"', from=3-2, to=3-3] +% \end{tikzcd} +% \end{equation*} +% Obviously, $s''$ and $s''^\mone$ are each other's inverse, thus $\appr_{X_1};\rel(F)(R)$ and $\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic. +% \begin{align*} +% Fp'_1\comp\varphi'_1\comp s''\comp\pi_1&\\ +% &=Fp'_1\comp Fs\comp\varphi_2\comp\pi_1\\ +% &=Fp_2\comp\varphi_2\comp\pi_1\\ +% &=i^2_1\comp\pi_2\\ +% &=i'^{2}_{2}\comp s_2\comp \pi_2 +% \end{align*} +% \begin{tikzcd}[ampersand replacement=\&] +% {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ +% \& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ +% {\appr_{X_2}} \&\& {FR^\op} \\ +% \& {\appr_{X_2}^\op} \& {FX_2} +% \arrow["{{{{{{{\pi_1}}}}}}}", from=1-1, to=1-2] +% \arrow["{s'}", dashed, from=1-1, to=2-2] +% \arrow["{{{{{{{\pi_2}}}}}}}"', from=1-1, to=3-1] +% \arrow["{s''}", from=1-2, to=2-3] +% \arrow["{{{{{{\pi'_2}}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{{\pi'_1}}}}}}"', from=2-2, to=4-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] +% \arrow["{\varphi'_1}", from=2-3, to=3-3] +% \arrow["{{{s_2}}}", from=3-1, to=4-2] +% \arrow["{Fp'_1}", from=3-3, to=4-3] +% \arrow["{i'^{2}_{2}}", from=4-2, to=4-3] +% \end{tikzcd} +% +% \begin{align*} +% Fp_2\comp\varphi_2\comp s''^\mone\comp\pi'_2&\\ +% &=Fp_2\comp Fs^\mone\comp\varphi'_1\comp\pi'_2\\ +% &=Fp'_1\comp\varphi'_1\comp\pi'_2\\ +% &=i'^{2}_{2}\comp\pi'_1\\ +% &=i^{2}_{1}\comp s_2^\mone\comp\pi'_1 +% \end{align*} +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \&\& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ +% \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ +% \&\& FR \\ +% {\appr_{X_2}^\op} \& {\appr_{X_2}} \& {FX_2} +% \arrow["{{{{{{\pi'_2}}}}}}", from=1-1, to=1-3] +% \arrow["{s'^\mone}"', dashed, from=1-1, to=2-2] +% \arrow["{{{{{{\pi'_1}}}}}}"', from=1-1, to=4-1] +% \arrow["{s''^\mone}", from=1-3, to=2-3] +% \arrow["{{{{{{{\pi_1}}}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{{{\pi_2}}}}}}}"', from=2-2, to=4-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] +% \arrow["{{{{{{{\varphi_2}}}}}}}", from=2-3, to=3-3] +% \arrow["{{{{{{{Fp_2}}}}}}}", from=3-3, to=4-3] +% \arrow["{{{s_2}^\mone}}"', from=4-1, to=4-2] +% \arrow["{{{{{{{i^2_1}}}}}}}"', from=4-2, to=4-3] +% \end{tikzcd} +% \end{equation*} +% So, we could prove that $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ and $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are isomorphic. $(\appr_{X_1};\rel(F)(R);\appr_{X_2})^\op$ is isomorphic to $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ by definition, so it is also isomorphic with $\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$.\qed +% %{\tiny +% % \begin{equation*} +% % \begin{tikzcd}[ampersand replacement=\&] +% % {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \& {\appr_{X_1}^\op} \& {FX_1} \\ +% % \& {FR^\op} \& {FX_1} \\ +% % {\appr_{X_2}^\op} \& {FX_2} \\ +% % {FX_2} +% % \arrow["{{{{{{\pi'_2}}}}}}"', from=1-1, to=1-2] +% % \arrow["{{{{{{\pi'_1}}}}}}", from=1-1, to=3-1] +% % \arrow["{{{{\varphi'_2}}}}", from=1-2, to=1-3] +% % \arrow[""{name=0, anchor=center, inner sep=0}, "{{{{\varphi'_1}}}}"', from=1-2, to=2-2] +% % \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] +% % \arrow["{{{{{{{i'^{1}_2}}}}}}}", from=1-3, to=1-4] +% % \arrow["{{{{{{{i'^{1}_1}}}}}}}"', from=1-3, to=2-3] +% % \arrow["{{{{{{{Fp'_2}}}}}}}", from=2-2, to=2-3] +% % \arrow["{{{{{{{Fp'_1}}}}}}}", from=2-2, to=3-2] +% % \arrow[""{name=1, anchor=center, inner sep=0}, from=3-1, to=3-2] +% % \arrow["{{{{{{{i'^{2}_1}}}}}}}", from=3-1, to=4-1] +% % \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-1, to=0] +% % \arrow["{{{{{{{i'^{2}_2}}}}}}}", from=1, to=3-2] +% % \end{tikzcd} +% % \end{equation*} +% %} +%\end{proof} +%\begin{prop} +% Having $\sigma\c R\to\appr_{X_2};\rel(F)(R);\appr_{X_1}$ and $\sigma^\op\c R^{\op}\to\appr_{X_1};\rel(F)(R^{\op});\appr_{X_2}$ gives rise to a morphism $\gamma\c R\to\rel(F)(R)$, and vice-versa. +%\end{prop} +%\begin{proof} +% {\tiny +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% R \&\&\&\& {X_1} \\ +% \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \& {FX_1} \& {X_1} \\ +% \&\& FR \& {FX_1} \& {\appr_{X_1}^\op} \\ +% \& {\appr_{X_2}} \& {FX_2} \& {FR^\op} \& {\rel(F)(R^\op);\appr_{X_1}^\op} \\ +% {X_2} \& {FX_2} \& {\appr_{X_2}^\op} \&\& {\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op} \\ +% \& {X_2} \&\&\&\& {R^\op} +% \arrow["{{{{{p_1}}}}}", from=1-1, to=1-5] +% \arrow["\sigma"', from=1-1, to=2-2] +% \arrow["{{{{{p_2}}}}}"', from=1-1, to=5-1] +% \arrow["\alpha", from=1-5, to=2-5] +% \arrow["{{{{{{\pi_1}}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{{\pi_2}}}}}}"', from=2-2, to=4-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] +% \arrow["{{{{{{\varphi_1}}}}}}", from=2-3, to=2-4] +% \arrow["{{{{{{\varphi_2}}}}}}", from=2-3, to=3-3] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] +% \arrow["{{{{{{i^1_1}}}}}}", from=2-4, to=2-5] +% \arrow["{{{{{{i^1_2}}}}}}", from=2-4, to=3-4] +% \arrow["{{s_1}}", from=2-4, to=3-5] +% \arrow["\alpha", from=2-6, to=2-5] +% \arrow["{{{{{{Fp_1}}}}}}", from=3-3, to=3-4] +% \arrow["{{{{{{Fp_2}}}}}}"', from=3-3, to=4-3] +% \arrow["Fs"', from=3-3, to=4-4] +% \arrow["{{{{{{i'^{1}_2}}}}}}", from=3-5, to=2-5] +% \arrow["{{{{{{i'^{1}_1}}}}}}"', from=3-5, to=3-4] +% \arrow["{{{{{{i^2_1}}}}}}"', from=4-2, to=4-3] +% \arrow["{{{{{{i^2_2}}}}}}"', from=4-2, to=5-2] +% \arrow["{{s_2}}"', from=4-2, to=5-3] +% \arrow["{{{{{{Fp'_2}}}}}}", from=4-4, to=3-4] +% \arrow["{{{{{{Fp'_1}}}}}}", from=4-4, to=4-3] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=225}, draw=none, from=4-5, to=3-4] +% \arrow["{{{\varphi'_2}}}", from=4-5, to=3-5] +% \arrow[""{name=0, anchor=center, inner sep=0}, "{{{\varphi'_1}}}"', from=4-5, to=4-4] +% \arrow["\beta"', from=5-1, to=5-2] +% \arrow[""{name=1, anchor=center, inner sep=0}, from=5-3, to=4-3] +% \arrow["{{{{{{i'^{2}_1}}}}}}", from=5-3, to=5-2] +% \arrow["{{{{{\pi'_2}}}}}"', from=5-5, to=4-5] +% \arrow["{{{{{\pi'_1}}}}}", from=5-5, to=5-3] +% \arrow["\beta"', from=6-2, to=5-2] +% \arrow["{{{{{p'_2}}}}}", from=6-6, to=2-6] +% \arrow["{{{{{\sigma^\op}}}}}"', from=6-6, to=5-5] +% \arrow["{{{{{p'_1}}}}}"', from=6-6, to=6-2] +% \arrow["{{{{{{i'^{2}_2}}}}}}", from=1, to=4-3] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=5-5, to=0] +% \end{tikzcd} +% \end{equation*} +% } +% ($\Leftarrow$): We assume that we have the morphism $\gamma\c R\to FR$ such that the following diagram commutes: +% \begin{equation} +% \begin{tikzcd}[ampersand replacement=\&] +% {X_2} \& R \& {X_1} \\ +% {FX_2} \& FR \& {FX_1} +% \arrow["\beta"', from=1-1, to=2-1] +% \arrow["{p_2}"', from=1-2, to=1-1] +% \arrow["{p_1}", from=1-2, to=1-3] +% \arrow["\gamma", from=1-2, to=2-2] +% \arrow["\alpha", from=1-3, to=2-3] +% \arrow["{Fp_2}", from=2-2, to=2-1] +% \arrow["{Fp_1}"', from=2-2, to=2-3] +% \end{tikzcd} +% \end{equation} +% Since $\appr_{X_1}$ and $\appr_{X_1}$ preorders, they each have a morphism $\refl$ that pre-composed with their projections gives identity. As it is depicted in the following diagram the pullback property of ${\appr_{X_1};\rel(F)(R)}$ gives us $\sigma'\c R\to{\appr_{X_1};\rel(F)(R)}$ in the following commutative diagram: +% \begin{equation}\label{eq:diag-thm-sig'} +% \begin{tikzcd}[ampersand replacement=\&] +% R \& {X_1} \& {FX_1} \\ +% \& {\appr_{X_1};\rel(F)(R)} \& {\appr_{X_1}} \\ +% \& FR \& {FX_1} +% \arrow["{p_1}", from=1-1, to=1-2] +% \arrow["{\sigma'}", dashed, from=1-1, to=2-2] +% \arrow["\gamma"', bend right=30, from=1-1, to=3-2] +% \arrow["\alpha", from=1-2, to=1-3] +% \arrow["\refl", from=1-3, to=2-3] +% \arrow["{\varphi_1}", from=2-2, to=2-3] +% \arrow["{\varphi_2}", from=2-2, to=3-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] +% \arrow["{i_2^1}", from=2-3, to=3-3] +% \arrow["{Fp_1}"', from=3-2, to=3-3] +% \end{tikzcd} +% \end{equation} +% Then the pullback property of $\appr_{X_1};\rel(F)(R);\appr_{X_2}$ gives us the existence of $\sigma\c R\to \appr_{X_1};\rel(F)(R);\appr_{X_2}$ in the following commutative diagram: +% \begin{equation}\label{eq:diag-thm-sig} +% \begin{tikzcd}[ampersand replacement=\&] +% {X_2} \&\&\& R \\ +% \& {\appr_{X_1};\rel(F)(R);\appr_{X_2}} \& {\appr_{X_1};\rel(F)(R)} \\ +% \&\& FR \\ +% {FX_2} \& {\appr_{X_2}} \& {FX_2} +% \arrow["\beta"', from=1-1, to=4-1] +% \arrow["{p_2}"', from=1-4, to=1-1] +% \arrow["\sigma"', dashed, from=1-4, to=2-2] +% \arrow["{\sigma'}", from=1-4, to=2-3] +% \arrow["\gamma", bend left=40, from=1-4, to=3-3] +% \arrow["{\pi_1}", from=2-2, to=2-3] +% \arrow["{\pi_2}"', from=2-2, to=4-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-3] +% \arrow["{\varphi_2}", from=2-3, to=3-3] +% \arrow["{Fp_2}", from=3-3, to=4-3] +% \arrow["\refl"', from=4-1, to=4-2] +% \arrow["{i_1^2}"', from=4-2, to=4-3] +% \end{tikzcd} +% \end{equation} +% Now, we show that $\sigma$ is a simulation: +% \begin{align*} +% i^1_1\comp\varphi_1\comp\pi_1\comp\sigma&&\\ +% &=i^1_1\comp\varphi_1\comp\sigma'&\by{\eqref{eq:diag-thm-sig}}\\ +% &=i^1_1\comp\refl\comp\alpha\comp p_1&\by{\eqref{eq:diag-thm-sig'}}\\ +% &=\alpha\comp p_1& +% \end{align*} +% \begin{align*} +% i^2_2\comp\pi_2\comp\sigma&&\\ +% &=i^2_2\comp\refl\comp\beta\comp p_2&\by{\eqref{eq:diag-thm-sig}}\\ +% &=\beta\comp p_2 +% \end{align*} +% Considering that $s\c R\to R^\op$ and $s'\c\appr_{X_1};\rel(F)(R);\appr_{X_2}\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ are swapping isomorphisms, We set $\sigma^\op\c R^\op\to\appr_{X_2}^\op;\rel(F)(R^\op);\appr_{X_1}^\op$ to be $\sigma^\op=s'\comp\sigma\comp s^\mone$. Now, we show that $\sigma'$ is a simulation: +% \begin{align*} +% i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp \sigma^\op&\\ +% &=i'^{1}_{2}\comp\varphi'_2\comp\pi'_2\comp s'\comp\sigma\comp s^\mone\\ +% &=i^{1}_{1}\comp\varphi_1\comp\pi_1\comp\sigma\comp s^\mone\\ +% &=\alpha\comp p_1\comp s^\mone\\ +% &=\alpha\comp p'_2 +% \end{align*} +% \begin{align*} +% i'^{2}_{1}\comp\pi'_1\comp\sigma^\op=&\\ +% &=i'^{2}_{1}\comp\pi'_1\comp s'\comp\sigma\comp s^\mone\\ +% &=i_2^2\comp\pi_2\comp\sigma\comp s^\mone\\ +% &=\beta\comp p_2\comp s^\mone\\ +% &=\beta\comp p'_1 +% \end{align*} +%\end{proof} +%% +%\subsection{Simulation with one relation composition} +%We recall everything we had in the previous section. Although we want to work with the functor that takes $R\subseteq X_1\times X_2$ and gives $\rel(F)(R);\appr_{X_2}$. +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% {\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \\ +% {\appr_{X_2}} \& {FX_2} \\ +% {FX_2} +% \arrow["{{{{{{{{\pi_1}}}}}}}}", from=1-1, to=1-2] +% \arrow["{{{{{{{{\pi_2}}}}}}}}"', from=1-1, to=2-1] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] +% \arrow["{Fp_1}", from=1-2, to=1-3] +% \arrow["{{{{{{{{Fp_2}}}}}}}}", from=1-2, to=2-2] +% \arrow["{{{{{{{{i_1}}}}}}}}"', from=2-1, to=2-2] +% \arrow["{{{{{{{{i_2}}}}}}}}"', from=2-1, to=3-1] +% \end{tikzcd} +%\end{equation*} +%% +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% R \&\&\& {X_1} \\ +% \& {\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \& {X_1} \\ +% \& {\appr_{X_2}} \& {FX_2} \& FR \\ +% {X_2} \& {FX_2} \& {\appr_{X_2}^\op} \& {\rel(F)(R);\appr_{X_2}^\op} \\ +% \& {X_2} \&\&\& R +% \arrow["{{p_1}}", from=1-1, to=1-4] +% \arrow["\sigma", from=1-1, to=2-2] +% \arrow["{{p_2}}"', from=1-1, to=4-1] +% \arrow["\alpha", from=1-4, to=2-4] +% \arrow["{{{{{{{{{\pi_1}}}}}}}}}", from=2-2, to=2-3] +% \arrow["{{{{{{{{{\pi_2}}}}}}}}}"', from=2-2, to=3-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] +% \arrow["{{Fp_1}}", from=2-3, to=2-4] +% \arrow["{{Fp_2}}", from=2-3, to=3-3] +% \arrow["\alpha"', from=2-5, to=2-4] +% \arrow["{{{{{{{{{i_1}}}}}}}}}"', from=3-2, to=3-3] +% \arrow["{{{{{{{{{i_2}}}}}}}}}"', from=3-2, to=4-2] +% \arrow["{Fp_1}"', from=3-4, to=2-4] +% \arrow["{Fp_2}", from=3-4, to=3-3] +% \arrow["\beta"', from=4-1, to=4-2] +% \arrow["{i'_1}", from=4-3, to=3-3] +% \arrow["{i'_2}", from=4-3, to=4-2] +% \arrow["{\pi'_1}"', from=4-4, to=3-4] +% \arrow["{\pi'_2}", from=4-4, to=4-3] +% \arrow["\beta", from=5-2, to=4-2] +% \arrow[from=5-5, to=2-5] +% \arrow["{\sigma^\op}"', from=5-5, to=4-4] +% \arrow["{p_2}", from=5-5, to=5-2] +% \end{tikzcd} +%\end{equation*} +%% +%\begin{prop} +% Assuming $R\subseteq X\times X$, then if we have $\sigma\c R\to\rel(F)(R);\appr_{X}$ as a simulation for $R$, and $R$ is reflexive, then we have $\gamma\c R\to\rel(F)(R)$ as a bisimulation for $R$, and vice-versa. +%\end{prop} +%\begin{proof} +% $(\Rightarrow):$ +% \begin{align*} +% Fp_2\comp\pi_1\comp\sigma&&\\ +% &=i_1\comp\pi_2\comp\sigma\\ +% &=i'_2\comp s\comp\pi_2\comp\sigma\\ +% &= +% \end{align*} +%\end{proof} +%\subsection{Using Lax Pullbacks (Comma Objects) to Model Simulation} +%A big concern with this approach is that Comma Objects are defined in a 2-category, so we can not define them in $\Set$, while our main inspirational example is coming from $\Set$. % -\subsection{Simulation with one relation composition} -We recall everything we had in the previous section. Although we want to work with the functor that takes $R\subseteq X_1\times X_2$ and gives $\rel(F)(R);\appr_{X_2}$. -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - {\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \\ - {\appr_{X_2}} \& {FX_2} \\ - {FX_2} - \arrow["{{{{{{{{\pi_1}}}}}}}}", from=1-1, to=1-2] - \arrow["{{{{{{{{\pi_2}}}}}}}}"', from=1-1, to=2-1] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] - \arrow["{Fp_1}", from=1-2, to=1-3] - \arrow["{{{{{{{{Fp_2}}}}}}}}", from=1-2, to=2-2] - \arrow["{{{{{{{{i_1}}}}}}}}"', from=2-1, to=2-2] - \arrow["{{{{{{{{i_2}}}}}}}}"', from=2-1, to=3-1] - \end{tikzcd} -\end{equation*} +%\subsection{Working in $\Set$ First, Like Hughes and Jacobs} % -\begin{equation*} - \begin{tikzcd}[ampersand replacement=\&] - R \&\&\& {X_1} \\ - \& {\rel(F)(R);\appr_{X_2}} \& FR \& {FX_1} \& {X_1} \\ - \& {\appr_{X_2}} \& {FX_2} \& FR \\ - {X_2} \& {FX_2} \& {\appr_{X_2}^\op} \& {\rel(F)(R);\appr_{X_2}^\op} \\ - \& {X_2} \&\&\& R - \arrow["{{p_1}}", from=1-1, to=1-4] - \arrow["\sigma", from=1-1, to=2-2] - \arrow["{{p_2}}"', from=1-1, to=4-1] - \arrow["\alpha", from=1-4, to=2-4] - \arrow["{{{{{{{{{\pi_1}}}}}}}}}", from=2-2, to=2-3] - \arrow["{{{{{{{{{\pi_2}}}}}}}}}"', from=2-2, to=3-2] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] - \arrow["{{Fp_1}}", from=2-3, to=2-4] - \arrow["{{Fp_2}}", from=2-3, to=3-3] - \arrow["\alpha"', from=2-5, to=2-4] - \arrow["{{{{{{{{{i_1}}}}}}}}}"', from=3-2, to=3-3] - \arrow["{{{{{{{{{i_2}}}}}}}}}"', from=3-2, to=4-2] - \arrow["{Fp_1}"', from=3-4, to=2-4] - \arrow["{Fp_2}", from=3-4, to=3-3] - \arrow["\beta"', from=4-1, to=4-2] - \arrow["{i'_1}", from=4-3, to=3-3] - \arrow["{i'_2}", from=4-3, to=4-2] - \arrow["{\pi'_1}"', from=4-4, to=3-4] - \arrow["{\pi'_2}", from=4-4, to=4-3] - \arrow["\beta", from=5-2, to=4-2] - \arrow[from=5-5, to=2-5] - \arrow["{\sigma^\op}"', from=5-5, to=4-4] - \arrow["{p_2}", from=5-5, to=5-2] - \end{tikzcd} -\end{equation*} -% -\begin{prop} - Assuming $R\subseteq X\times X$, then if we have $\sigma\c R\to\rel(F)(R);\appr_{X}$ as a simulation for $R$, and $R$ is reflexive, then we have $\gamma\c R\to\rel(F)(R)$ as a bisimulation for $R$, and vice-versa. -\end{prop} -\begin{proof} - $(\Rightarrow):$ - \begin{align*} - Fp_2\comp\pi_1\comp\sigma&&\\ - &=i_1\comp\pi_2\comp\sigma\\ - &=i'_2\comp s\comp\pi_2\comp\sigma\\ - &= - \end{align*} -\end{proof} -\subsection{Using Lax Pullbacks (Comma Objects) to Model Simulation} -A big concern with this approach is that Comma Objects are defined in a 2-category, so we can not define them in $\Set$, while our main inspirational example is coming from $\Set$. - -\subsection{Working in $\Set$ First, Like Hughes and Jacobs} - -\subsection{Choosing a suitable order for our setting} -Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term. +%\subsection{Choosing a suitable order for our setting} +%Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term. \section{Symmetric Simulation is a Bisimulation} \todo{Obviously, this chapter should be changed. All the definitions should be moved to somewhere else. You should start the chapter by giving your counter examples, and then presenting your proofs.} \begin{definition}[Graph]