\documentclass[envcountsect,runningheads,draft]{llncs} % fails \newcommand\hmmax{0} \newcommand\bmmax{0} \sloppy \usepackage[nosumlimits,nointlimits,nonamelimits]{amsmath} \usepackage{amssymb} \usepackage[colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final]{hyperref} \renewcommand{\subsectionautorefname}{Section}% \newcommand{\xTo}[1]{\,\xRightarrow{#1}\,} %\newcommand{\lbs}[1]{\,\xRightarrow{#1}\,} \newcommand{\dhat}[1]{\check{#1}} \usepackage{lineno} \linenumbers \usepackage{etoolbox} %% <- for \cspreto, \csappto %% Patch 'normal' math environments: \newcommand*\linenomathpatch[1]{% \cspreto{#1}{\linenomath}% \cspreto{#1*}{\linenomath}% \csappto{end#1}{\endlinenomath}% \csappto{end#1*}{\endlinenomath}% } \linenomathpatch{equation} \linenomathpatch{gather} \linenomathpatch{multline} \linenomathpatch{align} \linenomathpatch{alignat} \linenomathpatch{flalign} \usepackage[T1]{fontenc} \usepackage[final]{graphicx} \usepackage{color} %\renewcommand\UrlFont{\color{blue}\rmfamily} %\urlstyle{rm} % \usepackage{etoolbox} \usepackage{needspace} \usepackage{hypcap} \setcounter{tocdepth}{2} \spnewtheorem{thm}{Theorem}[section]{\bfseries}{\itshape} \spnewtheorem{cor}[thm]{Corollary}{\bfseries}{\itshape} \spnewtheorem{lem}[thm]{Lemma}{\bfseries}{\itshape} \spnewtheorem{prop}[thm]{Proposition}{\bfseries}{\itshape} \spnewtheorem{defn}[thm]{Definition}{\bfseries}{\upshape} \spnewtheorem{rem}[thm]{Remark}{\bfseries}{\upshape} \spnewtheorem{notation}[thm]{Notation}{\bfseries}{\upshape} \spnewtheorem{expl}[thm]{Example}{\bfseries}{\upshape} \spnewtheorem{assumption}[thm]{Assumption}{\bfseries}{\upshape} \renewenvironment{theorem}{\begin{thm}}{\end{thm}} \renewenvironment{corollary}{\begin{cor}}{\end{cor}} \renewenvironment{lemma}{\begin{lem}}{\end{lem}} \renewenvironment{proposition}{\begin{prop}}{\end{prop}} \renewenvironment{definition}{\begin{defn}}{\end{defn}} \renewenvironment{remark}{\begin{rem}}{\end{rem}} \renewenvironment{example}{\begin{expl}}{\end{expl}} %\renewcommand{\sectionautorefname}{Section}% %\renewcommand{\subsectionautorefname}{Section}% \let\vec\relax % \usepackage{accents} \newcommand\thickbar[1]{\accentset{\rule{.55em}{.6pt}}{#1}} \sloppy \usepackage{wasysym} %Pouya: I added this package for auxillary compositions. \usepackage{cancel} \usepackage{tikz-cd} \usetikzlibrary{arrows.meta} \usetikzlibrary{decorations} % Required for all decorations \usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag' \tikzset{ commutative diagrams/.cd, arrow style = tikz, diagrams = {>=stealth}, row sep = large, column sep = huge } \usepackage{textcomp} \usepackage{enumitem} %\setlist{itemsep=0ex} \setlist[itemize]{label={\small$\bullet$}} \BeforeBeginEnvironment{align}{\noindent\ignorespaces} \usepackage{todos} \usepackage{proof} \usepackage{xspace} \usepackage{bm} \input{catprog} %\usepackage{pict2e} %\DeclareRobustCommand{\pigpenA}{% % \begingroup\setlength{\untlength}{1em}% % \linethickness{.075em}% % \begin{picture}(1,.8) % \roundcap\roundjoin % \polyline(.2,.2)(.8,.2)(.8,.8) % \end{picture}% % \endgroup %} \newcommand{\lbs}[1]{ \mathrel{% \tikz{ \draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.3) -- node[inner sep=0pt,above=1.75pt,midway] {\scriptsize$#1$} (.5,.3); } } } \newcommand{\pbk}{\arrow[dr, phantom, "\text{\tiny\pigpenA}", pos=0.05]} \newcommand{\Fst}{\Pi_1} %{\oname{Fst}} \newcommand{\Snd}{\Pi_2} %{\oname{Snd}} \newcommand{\klstar}{\sharp} %% Kleisli star \newcommand{\istar}{\dagger} \newcommand{\mSv}{\mS_\val} \newcommand{\mSc}{\mS_\com} \newcommand{\mSl}{\mS_\lambda} \newcommand{\Sigmas}{\Sigma^\star} \newcommand{\ar}{\oname{ar}} \newcommand{\oWh}{\oname{while}} \newcommand{\oIf}{\oname{if}} \newcommand{\oPut}{\oname{put}} \newcommand{\oGet}{\oname{get}} \newcommand{\oSeq}{\oname{seq}} \newcommand{\app}{\,} \usepackage{proof} \newcommand{\inference}[2]{\infer{~#2~}{~#1~}} \newcommand{\St}{\Gamma} \newcommand{\exend}{\hfill{\rotatebox[origin=c]{45}{$\Box$}}} \makeatletter \let\dir@frac\frac \newcommand{\inv@frac}[2]{\dir@frac{#2}{#1}} \renewcommand{\frac}{\@ifstar{\inv@frac}{\dir@frac}} \makeatother %\renewcommand{\dar}{\kern1.2pt\operatorname{\downarrow}\kern1pt} \newcommand{\G}{\St} \newcommand{\D}{\Delta} %\usepackage{txfonts} %\usepackage{newtxtext,newtxmath} \newcommand{\mon}{\bullet} \newcommand{\monto}{\mathrel{-}\joinrel\mathrel{\bullet}} %{\multimapdot} \newcommand{\Pt}{V} \newcommand{\dc}{\mspace{\medmuskip};\mspace{.5\medmuskip}} \newcommand{\sep}{,\mspace{\medmuskip}} \newcommand{\xCL}{\textbf{xCL}\xspace} \newcommand{\xTCL}{\textbf{xTCL}\xspace} \newcommand{\Ty}{\mathsf{Ty}\xspace} \newcommand{\Tr}{\mathsf{Tr}\xspace} \newcommand{\arty}[2]{#1 \rightarrowtriangle #2} \newcommand{\initob}{\textbf{0}} \newcommand{\termob}{\textbf{1}} \newcommand{\tcomp}{\textsf{comp}} \newcommand{\unt}{\mathsf{unit}} \newcommand{\true}{\mathsf{true}} \newcommand{\false}{\mathsf{false}} \newcommand{\bool}{\mathsf{bool}} \newcommand{\fpc}{\mathsf{fix}} \newcommand{\casec}{\mathsf{if}} \newcommand{\ndet}{\oplus} %{\;\ensuremath{\boldsymbol{\pmb{\oplus}}}\;} \newcommand{\paral}{\parallel} %{\;\ensuremath{\boldsymbol{\pmb{\mid\mid}}}\;} \newcommand{\nDownarrow}{\cancel{\Downarrow}} \newcommand{\paralv}{\mathrel{% \mathchoice{\PARV}{\PARV}{\scriptsize\PARV}{\tiny\PARV} }} \def\PARV{{% \setbox0\hbox{$\parallel$}% \rlap{\hbox to \wd0{\hss\rule[-.5ex]{.75em}{.12ex}\hss}}\box0 }} \usepackage{ifdraft} \ifdraft{ % \usepackage{showframe} \usepackage{showlabels} \renewcommand{\showlabelfont}{\ttfamily\scriptsize} \usepackage[layout=footnote,draft]{fixme} % \usepackage[notcite,notref]{showkeys} % \renewcommand*\showkeyslabelformat[1]{% % \raisebox{1ex}{\raggedleft{\textit{\tiny #1}}} }{ \usepackage[layout=footnote,final]{fixme} } \FXRegisterAuthor{sg}{asg}{SG} % Sergey \FXRegisterAuthor{pp}{app}{PP} % Pouya \usepackage{savesym} \savesymbol{degree} \savesymbol{leftmoon} \savesymbol{rightmoon} \savesymbol{fullmoon} \savesymbol{newmoon} \savesymbol{diameter} \savesymbol{emptyset} \savesymbol{bigtimes} %\savesymbol{blacktriangleright} \savesymbol{triangleright} \savesymbol{langle} \savesymbol{rangle} \usepackage[matha,mathx]{mathabx} \restoresymbol{other}{langle} \restoresymbol{other}{rangle} \restoresymbol{other}{emptyset} \restoresymbol{other}{triangleright} \usepackage{adjustbox} % For size of diagrams. % document specific \newcommand{\val}{\mathsf{v}} \newcommand{\com}{\mathsf{c}} \newcommand{\nats}{\mathbb{N}} \newcommand{\ints}{\mathbb{Z}} \newcommand{\mS}{\mu\Sigma} \newcommand{\bss}{\oname{bs}} \renewcommand{\paragraph}[1]{\medskip\noindent{\bfseries\sffamily #1.}} \renewcommand{\comp}{\cdot} \newcommand{\dist}{\oname{dist}} \newcommand{\ldist}{\oname{dist}'} \newcommand{\zero}{\oname{o}} \newcommand{\suc}{\oname{s}} \newcommand{\init}{\oname{init}} \newcommand{\primr}{\oname{primr}} \newcommand{\peval}{\frak{p}} \newcommand{\teval}{\frak{t}} \newcommand{\neval}{\frak{n}} \newcommand{\rcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\RIGHTcircle$}}}} \newcommand{\lcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\LEFTcircle$}}}} \newcommand{\fcomp}{\mathbin{\raisebox{1pt}{\scalebox{.6}{$\CIRCLE$}}}}%Pouya: I added these three. \newcommand{\tsto}{\leftrightarrow} \newcommand{\ba}{\Downarrow} %\newcommand{\bba}{\pmb{\Downarrow}} \newcommand{\ssim}{\mathrel{\pmb{\sim}}} \newcommand{\hatssim }{\mathrel{\hat{\ssim}}} \newcommand{\dhatssim }{\mathrel{\dhat{\ssim}}} \newcommand{\klplus}{\boxplus} \newcommand{\coit}{\mathsf{coit}} \newcommand{\itt}{\mathsf{it}} \newcommand{\eval}{\mathsf{eval}} \newcommand{\refl}{\mathsf{refl}} \newcommand{\trans}{\mathsf{trans}} \newcommand{\preord}{\mathbf{PreOrd}} \newcommand{\rel}{\mathbf{Rel}} \newcommand{\gra}{\mathbf{Gra}} \newcommand{\obj}{\mathbf{Obj}} \newcommand{\bba}{ \mathrel{% \begin{tikzpicture}[baseline=-6pt] \draw[double, double distance=.75pt, -{Stealth[inset=0pt, angle=75:4pt]}] (0,.02) -- (0,-.28); \end{tikzpicture}% }% } \usepackage[final]{listings} \lstset{ language=Haskell %,xleftmargin=2.0cm , basicstyle=\small , commentstyle=\color{gray} , stringstyle=\itshape % string literal style , keepspaces=true % keeps spaces in text, useful for keeping indentation of code , numbers=none % possible values are (none, left, right) , identifierstyle={\itshape} , flexiblecolumns={true} , showstringspaces={false} %,mathescape={true} , captionpos=b , deletekeywords={join,return,Eval,Left,Either,Right,id,either,Void,Functor,Monad} % , morekeywords={Free} , emphstyle=\slshape , literate={\\}{{$\lambda$}}1 {->}{{$\rightarrow$}}2 , literate= {'}{$\,{}^\prime$\!}1 {+s}{{$\,$}}1 {\\}{{$\lambda$}}1 {lnot}{$\lnot$}3 {=>}{{$\Rightarrow$}}1 {<=}{{$\leq$}}1 {<<-}{{$\in$}}1 {<<=}{{$\subseteq$}}1 {>>=}{{$\gg\kern-1pt=$}}1 {++}{{$\varoplus$}}2 {|->}{{$\mapsto$}}1 {->}{{$\rightarrow$}}1 {->d}{{$\rightarrow_\delta$}}2 {->b}{{$\rightarrow_\beta$}}2 {->bd}{{$\rightarrow_{\beta\delta}^*$}}2 {::=}{{$:=$}}2 {:=}{{$\mapsto$}}1 {alpha}{{$\alpha$}}1 {UU}{{$\cup$}}1 {All}{{${\forall}\!\!\!\!$}}1 } \setcounter{totalnumber}{1} % No two figures in one page \begin{document}\allowdisplaybreaks \let\cedilla\c \renewcommand{\c}{\colon} % \title{Coalgebraic Simulation.} % %\titlerunning{Abbreviated paper title} % If the paper title is too long for the running head, you can set % an abbreviated paper title here % \author{Sergey Goncharov\inst{1}\orcidID{0000-0001-6924-8766} \and Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}} % \authorrunning{S.~Goncharov, P.~Partow} % First names are abbreviated in the running head. % If there are more than two authors, 'et al.' is used. % \institute{University of Birmingham, UK\\ \email{\{s.goncharov,p.partow\}@bham.ac.uk}} % \maketitle % typeset the header of the contribution % \begin{abstract} Hello simulation! \end{abstract} % % % \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*} \begin{lemma}\label{lem:norm-simp} Assuming that we have the following commutative diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ FX \& FR \& 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}", from=2-2, to=2-1] \arrow["{Fp_2}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} Then there exists $\sigma^\dagger\c R\to(FR)^\dagger$ in the following diagram that is also commutative: \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^\dagger}}", 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*} \end{lemma} \begin{proof} The proof is trivial considering that $\sigma^\dagger=e_{FR}\comp\sigma$, where $e_{FR}$ is the epimorphism in the epi-mono factorization of $\brks{Fp_1,Fp_2}$, as depicted in the following diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ FX \& FR \& FX \\ 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["\id"', from=2-1, to=3-1] \arrow["{Fp_1}", from=2-2, to=2-1] \arrow["{Fp_2}"', from=2-2, to=2-3] \arrow["{e_{FR}}", from=2-2, to=3-2] \arrow["\id", from=2-3, to=3-3] \arrow["{Fp_1^\dagger}", from=3-2, to=3-1] \arrow["{Fp_2^\dagger}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} \qed \end{proof} 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} \section{Relators} We start the discussion with answering the question that why there can be multiple simulation structures based on~\autoref{def:sim}. At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X} \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", dashed, from=1-2, to=2-2] \arrow["\alpha", from=1-3, to=2-3] \arrow["{{\mathcal{P}p_1}_\subseteq}", from=2-2, to=2-1] \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} It is defined as $\sigma(x_1,x_2)=(\alpha(x_1),\alpha(x_2))$. But $\sigma'$ in the following diagram is not unique: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} \arrow["\alpha"', from=1-1, to=2-1] \arrow["\subseteq"{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["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3] \arrow["{{\mathcal{P}p_1^\dagger}}", from=2-2, to=2-1] \arrow["{{\mathcal{P}p_2^\dagger}}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} Because assuming we have $\sigma$, for every given $\sigma'$ we can define a $\delta\c(\mathcal{P}R)^\dagger\to\subseteq;(\mathcal{P}R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ {\mathcal{P}X} \& {(\mathcal{P}R)^\dagger} \& {\mathcal{P}X} \\ {\mathcal{P}X} \& {\subseteq;(\mathcal{P}R)^\dagger;\subseteq} \& {\mathcal{P}X} \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["id"', from=2-1, to=3-1] \arrow["\delta", from=2-2, to=3-2] \arrow["id"', from=2-3, to=3-3] \arrow["{{\mathcal{P}p_1}_\subseteq}", from=3-2, to=3-1] \arrow["{{\mathcal{P}p_2}_\subseteq}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} $\delta$ is defined as the following: \begin{gather*} \delta(w)= \begin{cases} (\alpha(x_1),\alpha(x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w \\ w & \mathsf{o.w} \end{cases} \end{gather*} Now, we want to prove an abstraction of this statement. First, we need to spell out what $\appr;(FR)^\dagger;\appr$ is. We define relation compositions with pullbacks, so we have the following diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] {\appr;(FR)^\dagger;\appr} \& {\appr;(FR)^\dagger} \& {\appr} \& {FX} \\ \& (FR)^\dagger \& {FX} \\ {\appr} \& {FX} \\ {FX} \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}}}}}}}", from=1-3, to=1-4] \arrow["{{{{{{{i_2}}}}}}}", from=1-3, to=2-3] \arrow["{{{{{{{Fp_1^\dagger}}}}}}}", from=2-2, to=2-3] \arrow["{{{{{{{Fp_2^\dagger}}}}}}}"', from=2-2, to=3-2] \arrow["{{{{{{{i_1}}}}}}}"', from=3-1, to=3-2] \arrow["{{{{{{{i_2}}}}}}}"', from=3-1, to=4-1] \end{tikzcd} \end{equation*} Additionally, we make the abbreviations that ${Fp_1}_\appr=i_1\comp\varphi_1\comp\pi_1$ and ${Fp_2}_\appr=i_2\comp\pi_2$. \begin{prop} Assuming we have a morphism $\sigma'\c R\to(FR)^\dagger$ then exists $\delta\c(FR)^\dagger\to(\appr;(FR)^\dagger;\appr)^\dagger$ such that $\sigma=\delta\comp\sigma'$ that commutes in the following diagram: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ {FX} \& {(FR)^\dagger} \& {FX} \\ {FX} \& {(\appr;(FR)^\dagger;\appr)^\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["id"', from=2-1, to=3-1] \arrow["\delta", from=2-2, to=3-2] \arrow["id"', from=2-3, to=3-3] \arrow["{({Fp_1}_\appr)^\dagger}", from=3-2, to=3-1] \arrow["{({Fp_2}_\appr)^\dagger}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} \end{prop} \begin{proof} Ultimately, we need to define $\delta'\c(FR)\to\appr;(FR)^\dagger;\appr$, where $\delta=e_{\appr;(FR)^\dagger;\appr}\comp\delta'$, and $e_{\appr;(FR)^\dagger;\appr}\c\appr;(FR)^\dagger;\appr\to(\appr;(FR)^\dagger;\appr)^\dagger$ is the epimorphism in the epi-mono factorization of $\brks{{Fp_1}_\appr,{Fp_2}_\appr}$ because by~\autoref{lem:norm-simp} it suffices to show that the following diagram commutes: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& R \& X \\ FX \& {(FR)^\dagger} \& FX \\ FX \& {\appr;(FR)^\dagger;\appr} \& 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["id"', from=2-1, to=3-1] \arrow["{\delta'}", from=2-2, to=3-2] \arrow["id"', from=2-3, to=3-3] \arrow["{{{Fp_1}_\appr}}", from=3-2, to=3-1] \arrow["{{{Fp_2}_\appr}}"', from=3-2, to=3-3] \end{tikzcd} \end{equation*} So, we need to define $\delta'$. \end{proof} \end{document}