From 41912f4e54c84bbf99221fb41fea5e8da71e157d Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 16 Apr 2026 14:16:14 +0100 Subject: [PATCH] init --- draft/draft.tex | 1375 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 1374 insertions(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index fcb8cfe..c35338e 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -347,7 +347,7 @@ \renewcommand{\c}{\colon} % -\title{Weak Similarity for Strongly Separated HO-GSOS.} +\title{Coalgebraic Simulation.} % %\titlerunning{Abbreviated paper title} % If the paper title is too long for the running head, you can set @@ -371,7 +371,1380 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}} % % % +\section{Coalgebraic Simulation} +We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$. +\begin{definition}[A Preorder Over a Functor] + Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& \preord \\ + \Set \& \Set + \arrow[from=1-2, to=2-2] + \arrow["\appr", from=2-1, to=1-2] + \arrow["F"', from=2-1, to=2-2] + \end{tikzcd} + \end{equation*} +\end{definition} +% +\begin{definition}[Relation Lifting] + Assuming $F\c\Set\to\Set$ is a functor, then we call $\rel(F)\c\rel\to\rel$ a relation lifting of $F$, where the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \rel \&\& \rel \\ + {\Set\times\Set} \&\& {\Set\times\Set} + \arrow["{\rel(F)}", from=1-1, to=1-3] + \arrow[from=1-1, to=2-1] + \arrow[from=1-3, to=2-3] + \arrow["{F\times F}"', from=2-1, to=2-3] + \end{tikzcd} + \end{equation*} +\end{definition} +% +We take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $F$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$. +\begin{definition}[Bisimulation] + For a functor $F\c\Set\to\Set$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$. +\end{definition} +% +\begin{prop} + Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\Set\times\Set$, then the following diagram commutes, and vice-versa: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + {X_1} \& R \& {X_2} \\ + {FX_1} \& FR \& {FX_2} + \arrow["{\beta_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["\beta", from=1-2, to=2-2] + \arrow["{\beta_2}", from=1-3, to=2-3] + \arrow["{Fp_1}", from=2-2, to=2-1] + \arrow["{Fp_2}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} +\end{prop} +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=\&] + % {\appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}} \& {\appr_{X_2};\rel(B(\mS,-))(E)} \& {\appr_{X_2}} \& {B(\mS,X_2)} \\ + % \& {B(\mS,E)} \& {B(\mS,FX_2)} \\ + % {\appr_{X_1}} \& {B(\mS,X_1)} \\ + % {B(\mS,X_1)} + % \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, rotate=45}, draw=none, from=1-2, to=2-3] + % \arrow["{i^2_1}", from=1-3, to=1-4] + % \arrow["{i^2_2}", from=1-3, to=2-3] + % \arrow["{B(\mS,p_2)}", from=2-2, to=2-3] + % \arrow["{B(\mS,p_1)}"', from=2-2, to=3-2] + % \arrow["{i^1_1}"', from=3-1, to=3-2] + % \arrow["{i^1_2}"', from=3-1, to=4-1] + % \end{tikzcd} +%\end{equation*} +% +%So, we call $\sigma\c E\to \appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}$ a $B(\mS,-)$-simulation iff the following diagram commutes: +%\begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] + % {X_2} \& E \& {X_1} \\ + % {B(\mS,X_2)} \& {\appr_{X_2};\rel(B(\mS,-))(E);\appr_{X_1}} \& {B(\mS,X_1)} \\ + % {\appr_{X_1}} \& {\appr_{X_2};\rel(B(\mS,-))(E)} \& {\appr_{X_2}} + % \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["\sigma", from=1-2, to=2-2] + % \arrow["\alpha", from=1-3, to=2-3] + % \arrow["{\pi_2}", from=2-2, to=3-1] + % \arrow["{\pi_1}"', from=2-2, to=3-2] + % \arrow["{i_2^1}", from=3-1, to=2-1] + % \arrow["{\varphi_1}"', from=3-2, to=3-3] + % \arrow["{i_1^2}"', from=3-3, to=2-3] + % \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} +% +\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{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. +\section{Symmetric Simulation is Bisimulation} +\begin{definition}[Graph] + In a category $\BC$ a graph is a tuple $(R,X)$ of the following form: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& R \& \\ + X \&\& X + \arrow["{p_1}"', from=1-2, to=2-1] + \arrow["{p_2}", from=1-2, to=2-3] + \end{tikzcd} + \end{equation*} + Graphs over $\BC$ form a category that we show by $\gra(\BC)$. +\end{definition} +\begin{definition}[Symmetric Graph] + A graph $(R,X)$ is symmetric iff there exists an endomorphism $s\c R\to R$, such that the following diagram commutes + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + X \& R \& X + \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*} + and $s\comp s=\id$. We call $s$ a \emph{swap} for $R$. +\end{definition} +\begin{lemma}\label{lem:gra-sym} + Symmetry of a graphs over preserved a functor. +\end{lemma} +\begin{definition}[Relation] + A relation in a category $\BC$ is a graph $(R,X)$ where $\brks{p_1,p_2}\c R \to X\times Y$ is monic. Relations over $\BC$ form a category that we show by $\rel(\BC)$. +\end{definition} +\begin{definition}[Jointly Monic] + A pair of morphisms $p_1,p_2\c R\to X$ is jointly monic iff for every pair of morphisms $f,g\c A \to R$ assuming that $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$ then $f=g$. +\end{definition} +\begin{prop}\label{prop:rel-joi-mon} + A graph $(R,X)$ is a relation iff $p_1$ and $p_2$ are jointly monic. +\end{prop} +\begin{proof} + ($\Rightarrow$): We assume that for morphisms $f,g\c A\to R$ we have $p_1\comp f=p_1\comp g$ and $p_2\comp f=p_2\comp g$, and we want to prove that $f=g$. Assuming that $\pi_1,\pi_2\c X\times X\to X$ are projections of $X\times X$, then we have: + \begin{align*} + \brks{p_1,p_2}\comp f&\\ + =&\brks{p_1\comp f,p_2\comp f}\\ + =&\brks{p_1\comp g,p_2\comp g}\\ + =&\brks{p_1,p_2}\comp g + \end{align*} + Since $\brks{p_1,p_2}$ is moinc, from $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we get $f=g$. + + ($\Leftarrow$): Assuming for some morphisms $f,g\c A\to R$ we have $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we need to prove $f=g$. From $\brks{p_1,p_2}\comp f=\brks{p_1,p_2}\comp g$ we get $\brks{p_1\comp f,p_2\comp f}=\brks{p_1\comp g,p_2\comp g}$. Assuming that $\pi_1,\pi_2\c X\times X\to X$ are projections of $X\times X$, then we have $\pi_1\comp\brks{p_1\comp f,p_2\comp f}=\pi_1\comp\brks{p_1\comp g,p_2\comp g}$, and then $p_1\comp f=p_1\comp g$. Similarly we also get $p_2\comp f=p_2\comp g$. So, since $p_1$ and $p_2$ are jointly monic, then we have $f=g$.\qed +\end{proof} +We need to work with endofunctors over $\BC$ that are lifted over $\rel(\BC)$, for which we need to first define endofunctors lifted over $\gra(\BC)$. +Lifting from $\BC$ to $\gra(\BC)$ is easy. For $F\c\BC\to\BC$ we define $F_\gra\c\gra(\BC)\to\gra(\BC)$ as a functor that takes a graph $(R,X)$, and gives $(FR,FX)$, were $F$ is also applied on legs of the graph, i.e., $p_1,p_2\c R\to X$, so, we get the following graph: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& FR \& \\ + FX \&\& FX + \arrow["{Fp_1}"', from=1-2, to=2-1] + \arrow["{Fp_2}", from=1-2, to=2-3] + \end{tikzcd} +\end{equation*} +This lifting does not work for $\rel$. As an example, if we set $F$ to be the powerset functor $\mathcal{P}$, then $(\mathcal{P}R,\mathcal{P}X)$ is not necessarily a relation anymore. For example, if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, then taking $\{\{(1,0),(0,1),(0,0),(1,1)\}\}$ and $\{\{(1,0),(0,1),(0,0)\}\}$ as elements of $\mathcal{P}R$, the morphism $\brks{\mathcal{P}p_1,\mathcal{P}p_2}$ maps them both to $(\{0,1\},\{0,1\})$ so it is not monic. + +To cope with this, we assume the following epi-mono decomposition for $(R,X)\in\rel(\BC)$: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + R \& {R^\dagger} \&\& {X\times X} + \arrow["{e_R}"', two heads, from=1-1, to=1-2] + \arrow["{\brks{p_1,p_2}}", bend left=20, from=1-1, to=1-4] + \arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4] + \end{tikzcd} +\end{equation*} +We can define $(-)^\dagger$ as a functor from $\gra(\BC)\to\rel(\BC)$, then we define $F_\rel\c\rel(\BC)\to\rel(\BC)$ to take $(R,X)$ to the following relation: +\begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \& {(FR)^\dagger} \& \\ + FX \&\& FX \\ + \& {FX\times FX} + \arrow["{{{(Fp_1)^\dagger}}}"', from=1-2, to=2-1] + \arrow["{{{(Fp_2)^\dagger}}}", from=1-2, to=2-3] + \arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2] + \end{tikzcd} +\end{equation*} +We show this relation with $F_\rel(R,X)$. +\begin{definition}[Simulation]\label{def:sim} + A coalgebra $\sigma\c R\to (FR)^\dagger$ is a simulation over the $F$-coalgebra $\alpha\c X\to FX$ iff the following diagram is lax-commutative: + \begin{equation}\label{eq:diag-lax-sim} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& (FR)^\dagger \& FX + \arrow["\alpha"', from=1-1, to=2-1] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["{p_1}"', from=1-2, to=1-1] + \arrow["{p_2}", from=1-2, to=1-3] + \arrow["\sigma", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1] + \arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation} +\end{definition} +\begin{definition}[Bisimulation]\label{def:bisim} + The morphism $\sigma$ in~\autoref{def:sim} is a bisimulation iff the mentioned diagram is fully commutative. +\end{definition} +\begin{remark} + The mentioned definition of bisimulation is actually, the classical one in the literature that is to have the following commutative diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \\ + FX \& (FR)^\dagger \& FX + \arrow["\alpha"', 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["\sigma", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["{{(Fp_1)^\dagger}}", from=2-2, to=2-1] + \arrow["{{(Fp_2)^\dagger}}"', from=2-2, to=2-3] + \end{tikzcd} + \end{equation*} + It may look different because we have $FX$ and not $(FX)^\dagger$, but they are the same. + An object $X\in\obj(\BC)$ is $(X,X)\in\rel(\BC)$ having $\id$ as its legs. Meaning that the $(FX)^\dagger=FX$. +\end{remark} +% +\begin{prop}\label{prop:iff-sim-bsim} + Assuming that we have a bisimulation $\sigma$ for $R$, we have the following equation: + \begin{gather*} + \sigma\comp s=(Fs)^\dagger\comp\sigma + \end{gather*} +\end{prop} +\begin{proof} + We recall that by~\autoref{lem:gra-sym}, $F_\rel(R,X)$ is symmetric with the swap $(Fs)^\dagger$. Assuming that $\sigma$ is a bisimulation, we have the following commutative diagram: + \begin{equation}\label{eq:diag-sym-rel} + \begin{tikzcd}[ampersand replacement=\&] + \& R \& \\ + X \& R \& X \\ + FX \& (FR)^\dagger \& FX \\ + \& (FR)^\dagger + \arrow["{p_2}"', bend right=20, from=1-2, to=2-1] + \arrow["s", from=1-2, to=2-2] + \arrow["{p_1}", bend left=20, from=1-2, to=2-3] + \arrow["\alpha"', from=2-1, to=3-1] + \arrow["{p_1}"', from=2-2, to=2-1] + \arrow["{p_2}", from=2-2, to=2-3] + \arrow["\sigma", from=2-2, to=3-2] + \arrow["\alpha", from=2-3, to=3-3] + \arrow["{(Fp_2)^\dagger}", bend left=20, from=4-2, to=3-1] + \arrow["{(Fp_1)^\dagger}", from=3-2, to=3-1] + \arrow["{(Fp_2)^\dagger}"', from=3-2, to=3-3] + \arrow["(Fs)^\dagger", from=3-2, to=4-2] + \arrow["{(Fp_1)^\dagger}"', bend right=20, from=4-2, to=3-3] + \end{tikzcd} + \end{equation} + And it entails that the following diagrams are also commutative: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& R \& X \& X \& R \& X \\ + FX \& (FR)^\dagger \& FX \& FX \& (FR)^\dagger \& FX + \arrow["\alpha"', 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["{\sigma\comp s}", from=1-2, to=2-2] + \arrow["\alpha", from=1-3, to=2-3] + \arrow["\alpha"', from=1-4, to=2-4] + \arrow["{p_2}"', from=1-5, to=1-4] + \arrow["{p_1}", from=1-5, to=1-6] + \arrow["{(Fs)^\dagger\comp \sigma}", from=1-5, to=2-5] + \arrow["\alpha", from=1-6, to=2-6] + \arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1] + \arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3] + \arrow["{(Fp_1)^\dagger}", from=2-5, to=2-4] + \arrow["{(Fp_2)^\dagger}"', from=2-5, to=2-6] + \end{tikzcd} + \end{equation*} + So, since $(Fp_1)^\dagger$ and $(Fp_2)^\dagger$ are jointly monic (because $F_\rel(R,X)$ is a relation and~\autoref{prop:rel-joi-mon}) we have $\sigma\comp s=(Fs)^\dagger\comp\sigma$.\qed +\end{proof} +% +\begin{cor} + Assuming $\sigma_1$ and $\sigma_2$ are simulations of type $R\to (FR)^\dagger$, and $R$ is symmetric and both $\sigma_1$ and $\sigma_2$ satisfy the following property: + \begin{gather*} + (Fs)^\dagger\comp\sigma=\sigma\comp s + \end{gather*} + Then $\sigma_1=\sigma_2$. +\end{cor} +\begin{proof} + As the mentioned property is equivalent with $\sigma$ being a bisimulation, and bisimulation is unique, then $\sigma_1=\sigma_2$. +\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}$, $\sqsubseteq=\Delta\cup\{(C_1,C_2),(C_2,C'_2)\}$, and the coalgebra $\alpha$ is defined with the following set of reductions: +\begin{gather*} + A\to C_1\qquad B\to C_2\qquad C_1\to C_1\qquad C_2\to C_2\qquad C'_2\to C_2 +\end{gather*} +And finally, we define $\sigma$ as follows: +\begin{gather*} + \sigma(w)= + \begin{cases} + (\alpha\comp p_1(w),\alpha\comp p_2(w)) & w\neq (B,A) \\ + (C'_2,C_2) & w=(B,A) + \end{cases} +\end{gather*} + +It is easy to check that the conditions $\alpha\comp p_1\appr (Fp_1)^\dagger \comp\sigma$ and $(Fp_2)^\dagger \comp\sigma \appr \alpha\comp p_2$ are satisfied. For every $w\in R$ if $w\neq (B,A)$ then for $i\in\{1,2\}$, we have $\alpha\comp p_i= (Fp_i)^\dagger\comp\sigma$, and for $w=(B,A)$ we have $\alpha\comp p_1(B,A)=C_2\appr C'_2=(Fp_1)^\dagger \comp\sigma(B,A)$, and $\alpha\comp p_2(B,A)=C_1\appr C_2=(Fp_2)^\dagger \comp\sigma(B,A)$. +And $\sigma$ is not a coalgebraic bisimulation as $\alpha\comp p_1 (B,A)=C_2\neq C'_2=(Fp_1)^\dagger \comp\sigma(B,A)$. + +An interesting question would be to find out what conditions $\sigma$ should have (maybe we have the answer to this!~\autoref{prop:iff-sim-bsim}), or how it should be constructed (perhaps based on a given poset) so that it will also be a coalgebraic bisimulation if $R$ is symmetric. +Another avenue would be to give another definition for simulation that does not have this issue. + +Well! This counter example does not work! Because the described order $\appr$ does not satisfy the condition mentioned in Jacobs's paper. The condition is that the order on $FX$ should satisfy the property that for a morphism $f\c X\to Y$ the morphism $Ff\c FX\to FY$ preserves $\appr$. Probably, the only poset that has this property for $\mathbf{Id}$ is $\Delta$. If there is a counter-example, it is true for another functor. + +\begin{example} + Another counter-example! Assume that $F=\mathcal{P}$, and take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha(x)=X$ for every $x\in X$, and $\sigma$ is defined as below: + \begin{gather*} + \sigma(w)= + \begin{cases} + R & w\neq (1,3) \\ + R\setminus\{(1,2)\} & w=(1,3) + \end{cases} + \end{gather*} + In this scenario, $\sigma$ is a simulation, but it is not a bisimulation. It is a simulation since for every $w\in R$ we have $(\mathcal{P}p_1(\sigma(w)))=X$, thus for every $x\in X$, $\alpha(x)=X\subseteq X$. Also, $\mathcal{P}p_2(\sigma(w))\subseteq \alpha(p_2(w))$ as $\alpha(p_2(w))=X$ for every $w\in R$. But it is not a bisimulation, since $\alpha\comp p_2(1,3)=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=\{1,3\}$. +\end{example} +% +\begin{example} + And another counter-example!!! Assume that $F=\mathcal{P}$, and take $R=X\times X\setminus\{(1,3),(3,1)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined as below: + \begin{gather*} + \alpha(x)= + \begin{cases} + \{1,2\} & x=1 \\ + \{2,3\} & x=2\\ + \{3\} & x=3 + \end{cases} + \end{gather*} + And $\sigma_1$ is defined as below: + \begin{gather*} + \sigma_1(w)= + \begin{cases} + \{(1,2),(2,2)\} & w=(1,2) \\ + \{(2,1),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w\in\{(2,2),(3,2)\} \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_1(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w\in\{(2,2),(3,2)\} \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_1(w)= + \begin{cases} + \{2\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w\in\{(2,2),(3,2)\} \\ + \{3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + \sigma'_1(w)= + \begin{cases} + \{(1,2),(2,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,2),(3,3),(3,2)\} & w=(3,2) \\ + \{(2,3),(2,2),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma'_1(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(3,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma'_1(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(3,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + $\sigma'_1$ is not a simulation! + \begin{gather*} + \sigma''_1(w)= + \begin{cases} + \{(1,2)\} & w=(1,2) \\ + \{(2,1)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + + \begin{gather*} + \sigma_1\appr\sigma'_1\\ + \sigma_3\appr\sigma'_1\\ + \beta=\sigma'_1 + \end{gather*} + \begin{gather*} + (\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + \begin{cases} + \{(1,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(3,2),(3,3)\} & w=(3,2) \\ + \{(2,2),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(3,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_1\comp s(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(3,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + In this scenario, $\sigma_1$ is a simulation, but it is not a bisimulation. $\sigma'_1$, $\sigma''_1$ and $(\mathcal{P}s)^\dagger\comp\sigma_1\comp s$ are neither. We can not make $\sigma_1$ bigger here to make it a bisimulation as $\alpha\comp p_1(3,2)=\{3\}\subsetneq\{2,3\}=(\mathcal{P}p_1)^\dagger\comp\sigma_1(3,2)$. + + The following is also a simulation and not a bisimulation: + \begin{gather*} + \sigma_2(w)= + \begin{cases} + \{(1,2),(2,2)\} & w=(1,2) \\ + \{(2,1),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w\in\{(3,2),(3,3)\} + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_2(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w\in\{(3,2),(3,3)\} + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_2(w)= + \begin{cases} + \{2\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{3\} & w\in\{(3,2),(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + \sigma'_2(w)= + \begin{cases} + \{(1,2),(2,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(3,3),(3,2)\} & w=(3,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma'_2(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(3,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma'_2(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + \begin{cases} + \{(1,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(3,3),(3,2)\} & w=(3,2) \\ + \{(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(3,2) \\ + \{2\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_2\comp s(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(2,3) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + $\sigma_2$ is a simulation, $\sigma'_2$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_2\comp s$ is neither. + The following is both a simulation and a bisimulation: + \begin{gather*} + \sigma_3(w)= + \begin{cases} + \{(1,2),(2,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,2),(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_3(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_3(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + The following is also a simulation and not a bisimulation: + \begin{gather*} + \sigma_4(w)= + \begin{cases} + \{(1,2),(2,2),(3,2),(2,3),(3,3)\} & w=(1,2) \\ + \{(1,1),(2,1),(1,2),(2,2),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(1,2),(2,2),(3,2),(2,3),(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_4(w)= + \begin{cases} + \{1,2,3\} & w=(1,2) \\ + \{1,2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{1,2,3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_4(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + \sigma''_4(w)= + \begin{cases} + \{(1,2),(2,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2),(3,2)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,2),(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma''_4(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma''_4(w)= + \begin{cases} + \{2,3\} & w=(1,2) \\ + \{1,2\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + \begin{cases} + \{(1,1),(1,2),(2,1),(2,2),(2,3)\} & w=(1,2) \\ + \{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,3)\} & w=(2,2) \\ + \{(2,1),(2,2),(2,3),(3,2),(3,3)\} & w=(2,3) \\ + \{(3,2),(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma_4\comp s(w)= + \begin{cases} + \{1,2,3\} & w=(1,2) \\ + \{1,2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{1,2,3\} & w=(2,3) \\ + \{2,3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + $\sigma_4$ is a simulation, $\sigma''_4$ is a bisimulation, and $(\mathcal{P}s)^\dagger\comp\sigma_4\comp s$ is neither. + + The following is also a simulation and not a bisimulation: + \begin{gather*} + \sigma_5(w)= + \begin{cases} + \{(1,2),(2,2)\} & w=(1,2) \\ + \{(2,2),(3,2)\} & w=(2,1) \\ + \{(1,1),(2,1)\} & w=(1,1) \\ + \{(2,2),(3,2)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,3)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_5(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_5(w)= + \begin{cases} + \{2\} & w=(1,2) \\ + \{2\} & w=(2,1) \\ + \{1\} & w=(1,1) \\ + \{2\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + The following is also a simulation and not a bisimulation: + \begin{gather*} + \sigma_6(w)= + \begin{cases} + \{(1,2),(2,2)\} & w=(1,2) \\ + \{(2,1),(3,1)\} & w=(2,1) \\ + \{(1,2),(2,1)\} & w=(1,1) \\ + \{(2,3),(3,3)\} & w=(2,2) \\ + \{(2,3),(3,3)\} & w=(2,3) \\ + \{(3,2)\} & w=(3,2) \\ + \{(3,3)\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma_6(w)= + \begin{cases} + \{1,2\} & w=(1,2) \\ + \{2,3\} & w=(2,1) \\ + \{1,2\} & w=(1,1) \\ + \{2,3\} & w=(2,2) \\ + \{2,3\} & w=(2,3) \\ + \{3\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + (\mathcal{P}p_2)^\dagger\comp\sigma_6(w)= + \begin{cases} + \{2\} & w=(1,2) \\ + \{1\} & w=(2,1) \\ + \{2\} & w=(1,1) \\ + \{3\} & w=(2,2) \\ + \{3\} & w=(2,3) \\ + \{2\} & w=(3,2) \\ + \{3\} & w=(3,3) + \end{cases} + \end{gather*} + \begin{gather*} + \sigma'_2=\sigma'_5=\sigma'_6=\sigma_3=\sigma''_4 + \end{gather*} +\end{example} +% +If we define $\appr$ on simulations as +\begin{gather*} + \sigma_1\appr\sigma_2\iff \forall x_1,x_2\in X, (\mathcal{P}p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\mathcal{P}p_i)^\dagger\comp\sigma_2(x_1,x_2) +\end{gather*} +\begin{lemma} + $(Hom(R,(\mathcal{P}R)^\dagger),\appr)$ is a poset. +\end{lemma} +\begin{proof} + Reflexivity and transitivity are obvious. We need to prove anti-symmetry.\\ + \todo{Finish!} +\end{proof} +Then we have +\begin{equation*} + \begin{tikzcd} + {\sigma_6} && {\sigma_1} \\ + {\sigma_5} & {\sigma_2} & {\sigma_3} & {\sigma_4} + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-3, to=2-4] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-1, to=2-2] + \arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] + \arrow["\sqsubseteq"{description}, draw=none, from=2-2, to=2-3] + \arrow["\sqsubseteq"{description}, draw=none, from=2-3, to=2-4] + \end{tikzcd} +\end{equation*} +We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest are simulations. + +We can also define $\join$ and $\meet$ on morphisms as follows: +\begin{gather*} + \forall x_1,x_2\in X,\\ + \sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\ + \sigma_1 \meet \sigma_2 (x_1,x_2)= (\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2). +\end{gather*} +\begin{lemma}\label{lem:proj-dist-set} + For relations $R_1$ and $R_2$ the following equation holds: + \begin{gather*} + %(\mathcal{P}p_i)^\dagger(R_1\cup R_2)=(\mathcal{P}p_i)^\dagger(R_1)\cup(\mathcal{P}p_i)^\dagger(R_2) + (\mathcal{P}p_i)(R_1\cup R_2)=(\mathcal{P}p_i)(R_1)\cup(\mathcal{P}p_i)(R_2) + \end{gather*} +\end{lemma} +\begin{proof} + We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. + Assuming $x_1\in(\mathcal{P}p_1)^\dagger(R_1\cup R_2)$ then exists $x_2$ that $(x_1,x_2)\in R_1\cup R_2$, thus either $(x_1,x_2)\in R_1$ or $(x_1,x_2)\in R_2$, so we have $x_1\in(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$. + + Now, assuming that $x_1\in(\mathcal{P}p_1)^\dagger(R_1)\cup(\mathcal{P}p_1)^\dagger(R_2)$ either $x_1\in(\mathcal{P}p_1)^\dagger(R_1)$ or $x_1\in(\mathcal{P}p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\mathcal{P}p_1)^\dagger(R_j)$, where $j\in\{1,2\}$. + Then there exists $x_2$ that $(x_1,x_2)\in R_j$, then we have $(x_1,x_2)\in R_1\cup R_2$ that gives $x_1\in(\mathcal{P}p_1)^\dagger(R_1\cup R_2)$. + % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. + % + % First, we prove $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. + % Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. + % + % Now, we prove $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s\join(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: + % \begin{itemize} + % \item $y_1\in(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. + % \item $y_1\in(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. + % \end{itemize} \qed + % \todo{Rewrite the proof according to the statement!} +\end{proof} +\begin{lemma} + Assuming that $\sigma_1$ and $\sigma_2$ are simulation structures of type $R\to(\mathcal{P}R)^\dagger$, then $\sigma_1 \join \sigma_2$ and $\sigma_1 \meet \sigma_2$ are also simulation structures of the same type. +\end{lemma} +\begin{proof} + Since $\sigma_1$ and $\sigma_2$ are simulation structures, for every $(x_1,x_2)\in R$, for $i\in\{1,2\}$ we have: + \begin{gather} + \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2),\\ + (\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2). + \end{gather} + First, we prove the case for $\join$. Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following: + \begin{gather*} + \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2) + \end{gather*} + So, by~\autoref{lem:proj-dist-set} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$. + Similarly, we have $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following: + \begin{gather*} + (\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2) + \end{gather*} + So, by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))\subseteq\alpha(x_2)$. + + Now, we prove the case for $\meet$. For $\meet$ unlike $\join$ we need to prove that $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$. To achieve this, we need to show that assuming $\pi_1$, $\pi_2$ are projections of $\sigma_1\meet\sigma_2(x_1,x_2)$, then for $j\in\{1,2\}$ we have $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)\subseteq\mathcal{P}p_j(R)$. Since $(\mathcal{P}p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\mathcal{P}p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\mathcal{P}p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\mathcal{P}R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\mathcal{P}p_j)^\dagger\comp(\sigma_1\meet\sigma_2)(x_1,x_2)$.\ppnote{The last part of the proof is necessary because the type of the codomain of the definition of $\meet$ is not $(\mathcal{P}R)^\dagger$, but it is $\mathcal{P}X\times\mathcal{P}X$. Perhaps the epi-mono factorization must be used to cope with this in the abstract case.} + + For $j\in\{1,2\}$ we have + \begin{gather}\label{eq:proj-meet} + (\mathcal{P}p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\mathcal{P}p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_j)^\dagger\comp\sigma_2(x_1,x_2). + \end{gather} + Since $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have + \begin{gather*} + \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2), + \end{gather*} + so by~\eqref{eq:proj-meet} we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\mathcal{P}p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have + \begin{gather*} + (\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2), + \end{gather*} + so by~\eqref{eq:proj-meet} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))\subseteq\alpha(x_2)$.\qed +\end{proof} +\begin{lemma}\label{lem:sim-opsim-inc} + Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have: + \begin{enumerate} + \item $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ + \item $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$ + \end{enumerate} +\end{lemma} +\begin{proof} + We prove the second clause. + By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have + \begin{gather*} + \alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2),\\ + (\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2). + \end{gather*} + From $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)$, where + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp\sigma(x_2,x_1)=(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). + \end{gather*} + So, from $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$. Similarly, we can get the other inequation.\qed +\end{proof} +\begin{lemma}\label{lem:sim-bisim-inc} + Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, + \begin{enumerate} + \item if $\sigma\appr\beta$ then we have: + \begin{gather*} + \alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2), + \end{gather*} + and if $R$ is symmetric we have + \begin{gather*} + (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_2). + \end{gather*} + \item if $\beta\appr\sigma$ then we have: + \begin{gather*} + (\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2) + \end{gather*} + and if $R$ is symmetric we have + \begin{gather*} + \alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2). + \end{gather*} + \end{enumerate} +\end{lemma} +\begin{proof} + \begin{enumerate} + \item Since $\sigma$ is a simulation structure for an arbitrary $(x_1,x_2)\in R$ we have $\alpha(x_1)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\mathcal{P}p_1)\comp\sigma(x_1,x_2)\subseteq(\mathcal{P}p_1)\comp\beta(x_1,x_2)$, while $(\mathcal{P}p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$. Then because of the symmetry of $R$ the second clause is easily achievable by using the equations in~\eqref{eq:diag-sym-rel}. + \item This clause can be proven similar to (1). + \end{enumerate}\qed +\end{proof} +\begin{prop} + Assuming that $\sigma\c R\to(\mathcal{P}R)^\dagger$ is a simulation structure, and $\beta\c R\to(\mathcal{P}R)^\dagger$ is a bisimulation structure, + \begin{enumerate} + \item if $\sigma\appr\beta$ then we have: + \begin{gather*} + \beta=\sigma\join ((\mathcal{P}s)^\dagger\comp\sigma\comp s) + \end{gather*} + \item if $\beta\appr\sigma$ then we have: + \begin{gather*} + \beta=\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s) + \end{gather*} + \end{enumerate} +\end{prop} +\begin{proof} + 1. We need to prove that $\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. + By~\autoref{lem:sim-opsim-inc}.(1), for every $(x_1,x_2)\in R$, we have $(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\mathcal{P}p_1)^\dagger\comp\sigma\join(\mathcal{P}p_1)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. + + Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\join((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$. + + 2. We need to prove that $\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)$ is the bisimulation structure. + For $i\in\{1,2\}$, for every $(x_1,x_2)\in R$, we have: + {\small + \begin{align*} + &(\mathcal{P}p_i)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\ + &=(\mathcal{P}p_i)^\dagger\comp(((\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\ + &=(\mathcal{P}p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\mathcal{P}p_i)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2) + \end{align*} + } + + By~\autoref{lem:sim-opsim-inc}.(1), $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_1)^\dagger\comp((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\mathcal{P}p_1)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$. + + Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\mathcal{P}p_2)^\dagger\comp(\mathcal{P}s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\mathcal{P}p_2)^\dagger\comp(\sigma\meet((\mathcal{P}s)^\dagger\comp\sigma\comp s)(x_1,x_2))=\alpha(x_2)$.\qed +\end{proof} +\begin{cor} + Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism: + \begin{gather*} + (\bigjoin_{\sigma\in S}\sigma)\meet(\mathcal{P}s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s + \end{gather*} +\end{cor} + +\begin{lemma}\label{lem:alph-prod} + Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$, $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. +\end{lemma} +\begin{proof} + Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ for every $(x_1,x_2)$ as the following: + \begin{gather*} + \sigma(x_1,x_2)=\alpha(x_1)\times (\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2) + \end{gather*} + We have $\sigma(x_1,x_2)\in(\mathcal{P}R)^\dagger$, as $\alpha(x_1)\subseteq\mathcal{P}p_1(R)$ and $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\mathcal{P}p_2(R)$ are inherited from $\delta$ being a simulation structure. + Also, it obviously is a simulation as $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. +\end{proof} +\begin{prop} + Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then the following morphism is the bisimulation structure: + \begin{gather*} + (\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s + \end{gather*} +\end{prop} +\begin{proof} + For every $(x_1,x_2)\in R$ we have + \begin{gather*} + (\mathcal{P}p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= + (\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2), + \end{gather*} + and + \begin{gather*} + (\mathcal{P}p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)= + (\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2). + \end{gather*} + By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\mathcal{P}p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed +\end{proof} \end{document}