\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{\spa}{\mathbf{Span}}
\newcommand{\gra}{\mathbf{Gra}}
\newcommand{\obj}{\mathbf{Obj}}
\newcommand{\relar}{\mathbf{R}}
\newcommand{\emre}{\mathbf{L}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\powf}{\mathcal{P}}
\newcommand{\sappr}{\sqsupseteq}

\newcommand{\simeet}{%
	\mathbin{%
		\ooalign{%
			$\sqcap$\cr
			\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
		}%
	}%
}


\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 $\powf$, then $(\powf R,\powf 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 $\powf R$, the morphism $\brks{\powf p_1,\powf 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["\appr"{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["\appr"{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}$, $\appr=\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.

(But still!)We have a counter-example for a symmetric relation $R$ that has a witness to be a simulation, but that morphism does not serve as a witness for $R$ to be a bisimulation. In the category of sets we 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} 
		(X,X) & w\neq (1,3)  \\
		(X,X\setminus\{2\}) & w=(1,3)
	\end{cases}
\end{gather*}
In this scenario, $\sigma$ is a witness for $R$ to be a simulation, but it is not a witness for $R$ to be a bisimulation. $\sigma$ is a witness for $R$ to be a simulation since for every $w\in R$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\ddagger(\sigma(w)))=X$. Also, for every $w\in R$, $((\mathcal{P}p_2)^\ddagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\ddagger(\sigma(1,3))=X\setminus\{2\}$.
%
\begin{example}
	And another counter-example!!! Assume that $F=\powf $, 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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*}
		(\powf p_1)^\dagger\comp(\powf 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}
		(\powf p_2)^\dagger\comp(\powf 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 $(\powf 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\}=(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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*}
		(\powf p_1)^\dagger\comp(\powf 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}
		(\powf p_2)^\dagger\comp(\powf 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 $(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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*}
		(\powf p_1)^\dagger\comp(\powf 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}
		(\powf p_2)^\dagger\comp(\powf 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 $(\powf 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*}
		(\powf 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}
		(\powf 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*}
		(\powf 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}
		(\powf 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, (\powf p_i)^\dagger\comp\sigma_1(x_1,x_2)\subseteq(\powf p_i)^\dagger\comp\sigma_2(x_1,x_2)
\end{gather*}
\begin{lemma}
	$(Hom(R,(\powf 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.
\begin{definition}\label{def:join-meet}
We 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)= (\powf p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2).
\end{gather*}
\end{definition}
\begin{lemma}\label{lem:proj-dist-set}
	For relations $R_1$ and $R_2$ the following equation holds:
	\begin{gather*}
		%(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2)
		(\powf p_i)(R_1\cup R_2)=(\powf p_i)(R_1)\cup(\powf 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(\powf 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(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$, respectively. So, we have $x_1\in (\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$.
	
	Now, assuming that $x_1\in(\powf p_1)^\dagger(R_1)\cup(\powf p_1)^\dagger(R_2)$ either $x_1\in(\powf p_1)^\dagger(R_1)$ or $x_1\in(\powf p_1)^\dagger(R_2)$. Without loss of generality, we can assume $x_1\in(\powf 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(\powf 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 $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
	%	Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf 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(\powf 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(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$.
	%	
	%	Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have:
	%	\begin{itemize}
		%		\item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$.
		%		\item $y_1\in(\powf 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(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf 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(\powf 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(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2),\\
		(\powf 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(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$ we have the following:
	\begin{gather*}
		\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf 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(\powf p_1)^\dagger(\sigma_1(x_1,x_2)\cup \sigma_2(x_1,x_2))$.
	Similarly, we have $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$ that gives the following:
	\begin{gather*}
		(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cup (\powf 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 $(\powf 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(\powf 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\powf p_j(R)$. Since $(\powf p_j)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\powf p_j(R)$, we have $\pi_j\comp(\sigma_1 \meet \sigma_2) (x_1,x_2)\subseteq\powf p_j(R)$, so we have $\sigma_1\meet\sigma_2(x_1,x_2)\in(\powf R)^\dagger$, meaning that $\pi_j\comp(\sigma_1\meet\sigma_2)(x_1,x_2)=(\powf 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 $(\powf R)^\dagger$, but it is $\powf X\times\powf 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}
		(\powf p_j)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))=(\powf p_j)^\dagger\comp\sigma_1(x_1,x_2) \cap (\powf p_j)^\dagger\comp\sigma_2(x_1,x_2).
	\end{gather}	
	Since $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_i(x_1,x_2)$, we have
	\begin{gather*}
		\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_1)^\dagger\comp\sigma_2(x_1,x_2),
	\end{gather*}
	so by~\eqref{eq:proj-meet}  we have $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp(\sigma_1 \meet \sigma_2 (x_1,x_2))$. Similarly, since $(\powf p_2)^\dagger\comp\sigma_i(x_1,x_2)\subseteq\alpha(x_2)$, we have
	\begin{gather*}
		(\powf p_2)^\dagger\comp\sigma_1(x_1,x_2)\cap (\powf p_2)^\dagger\comp\sigma_2(x_1,x_2)\subseteq\alpha(x_2),
	\end{gather*}
	so by~\eqref{eq:proj-meet}  we have $(\powf 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(\powf R)^\dagger$ is a simulation structure, and $R$ is symmetric, then for all $(x_1,x_2)\in R$ we have:
	\begin{enumerate}
		\item $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$
		\item $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf 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(\powf p_1)^\dagger\comp\sigma(x_1,x_2),\\
		(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2).
	\end{gather*}
	From $\alpha(x_1)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ since $R$ is symmetric we get $\alpha(x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_2,x_1)$, where 
	\begin{gather*}
		(\powf p_1)^\dagger\comp\sigma(x_2,x_1)=(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2).
	\end{gather*}
	So, from $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf 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(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure, 
	\begin{enumerate}
		\item if $\sigma\appr\beta$ then we have:
		\begin{gather*}
			\alpha(x_1)=(\powf p_1)^\dagger\comp\sigma(x_1,x_2),
		\end{gather*}
		and if $R$ is symmetric we have
		\begin{gather*}
			(\powf p_2)^\dagger\comp(\powf 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*}
			(\powf 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)=(\powf p_1)^\dagger\comp(\powf 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(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. Since $\sigma\appr\beta$ we have $(\powf p_1)\comp\sigma(x_1,x_2)\subseteq(\powf p_1)\comp\beta(x_1,x_2)$, while $(\powf p_1)\comp\beta(x_1,x_2)=\alpha(x_1)$ by definition of bisimulation. So we have $\alpha(x_1)=(\powf 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(\powf R)^\dagger$ is a simulation structure, and $\beta\c R\to(\powf R)^\dagger$ is a bisimulation structure,
	\begin{enumerate}
		\item if $\sigma\appr\beta$ then we have:
		\begin{gather*}
			\beta=\sigma\join ((\powf s)^\dagger\comp\sigma\comp s)
		\end{gather*}
		\item if $\beta\appr\sigma$ then we have:
		\begin{gather*}
			\beta=\sigma\meet((\powf s)^\dagger\comp\sigma\comp s)
		\end{gather*}
	\end{enumerate}
\end{prop}
\begin{proof}
	1. We need to prove that $\sigma\join((\powf 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 $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(1), we have $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$. So, we have $(\powf p_1)^\dagger\comp\sigma\join(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)=\alpha(x_1)$, then by~\autoref{lem:proj-dist-set} we have $(\powf p_1)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
	
	Also, by~\autoref{lem:sim-bisim-inc}.(1) we have $(\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$. So, since we already have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ then by~\autoref{lem:proj-dist-set} we have $(\powf p_2)^\dagger\comp(\sigma\join((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_2)$.
	
	2. We need to prove that $\sigma\meet((\powf 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*}
			&(\powf p_i)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)\\
			&=(\powf p_i)^\dagger\comp(((\powf p_1)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2))\times((\powf p_2)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_2)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)))\\
			&=(\powf p_i)^\dagger\comp\sigma(x_1,x_2) \cap (\powf p_i)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)
		\end{align*}
	}
	
	By~\autoref{lem:sim-opsim-inc}.(1), $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)\subseteq (\powf p_1)^\dagger\comp\sigma(x_1,x_2)$, and by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s)(x_1,x_2)=\alpha(x_1)$, so we have $(\powf p_1)^\dagger\comp(\sigma\meet((\powf s)^\dagger\comp\sigma\comp s))(x_1,x_2)=\alpha(x_1)$.
	
	Also, by~\autoref{lem:sim-bisim-inc}.(2) we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_2)$, so, since by~\autoref{lem:sim-opsim-inc}.(2), we have $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq (\powf p_2)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$, so we have $(\powf p_2)^\dagger\comp(\sigma\meet((\powf 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 (\powf R)^\dagger$, then if the bisimulation morphism exists, it is equal with the following morphism:
	\begin{gather*}
		(\bigjoin_{\sigma\in S}\sigma)\meet(\powf s)^\dagger\comp(\bigjoin_{\sigma\in S}\sigma)\comp s
	\end{gather*}
\end{cor}

\begin{lemma}
	For every $S\in \powf R$,
	\begin{gather*}
		((\powf p_1)(S),(\powf p_2)(S))\in(\powf R)^\dagger\Leftrightarrow(\powf p_1)(S)\subseteq(\powf p_1)(R),(\powf p_2)(S)\subseteq(\powf p_2)(R)
	\end{gather*}
\end{lemma}
\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 (\powf R)^\dagger$, then there there exists a simulation structure $\sigma\in S$ that for every $(x_1,x_2)$,  $(\powf 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), (\powf p_2)^\dagger\comp\delta(x_1,x_2))
	\end{gather*}
	We have $\sigma(x_1,x_2)\in(\powf R)^\dagger$, as $\alpha(x_1)\subseteq\powf p_1(R)$ and $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\powf p_2(R)$ are inherited from $\delta$ being a simulation structure.
	Also, it obviously is a simulation as $(\powf p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\powf p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\powf p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. 
\end{proof}
\begin{prop}\label{prop:sym-rel-bisim}
	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\powf R)^\dagger$, then the following morphism is the bisimulation structure:
	\begin{gather*}
		(\bigmeet_{\sigma\in S}\sigma)\join(\powf 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*}
		(\powf p_1)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
		(\powf p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2),
	\end{gather*}
	and
	\begin{gather*}
		(\powf p_2)^\dagger\comp((\bigmeet_{\sigma\in S}\sigma)\join(\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=
		(\powf p_2)^\dagger\comp((\powf 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 $(\powf p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\powf 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 $(\powf p_2)^\dagger\comp((\powf s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed
\end{proof}
\section{Symmetric Simulation in Quantaloids}
We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices. 
Abstractly, first we define an operation that we need on morphisms that takes two simulation witnesses of type $R\to(FR)^\dagger$ to a morphism of type $R\to FX\times FX$:
\begin{gather*}
	\sigma_1\simeet\sigma_2=(Fp_1)^\dagger\comp\sigma_1\meet(Fp_1)^\dagger\comp\sigma_2\times(Fp_2)^\dagger\comp\sigma_1\meet(Fp_2)^\dagger\comp\sigma_2
\end{gather*}
\begin{lemma}\label{lem:alph-prod-abs}
	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that,  $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$. 
\end{lemma}
\begin{proof}
	Since $S\neq\emptyset$ there exists $\delta\in S$. We define $\sigma$ as the following:
	\begin{gather*}
		\sigma=\brks{(\alpha\comp p_1), (Fp_2)^\dagger\comp\delta}
	\end{gather*}
	We have $(Fp_1)^\dagger\comp\sigma$.
\end{proof}
\section{Relators}
\subsection{Two-way similarity in Hughes-Jacobs}
Hughes and Jacobs define two-way similarity as $\leq\cap\leq^\op$. They give a sufficient condition for the two-way similarity to be the bisimilarity. We discuss that this condition does not allow us to say that a symmetric simularity is a bisimilarity. The condition is:
\begin{gather*}
	\appr;(FR_1)^\dagger;\appr\quad\cap\quad\appr^\op;(FR_2)^\dagger;\appr^\op\qquad\subseteq\qquad(F(R_1\cap R_2))^\dagger
\end{gather*}
We need the case that $R_1=R_2$, and we refer to it with $R$. So, we need to have
\begin{gather*}
	\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op\qquad\subseteq\qquad(FR)^\dagger.
\end{gather*}
Assuming $(x_1,x_2)\quad\in\quad	\appr;(FR)^\dagger;\appr\quad\cap\quad\appr^\op;(FR)^\dagger;\appr^\op$ means that there exist $(u,v),(u',v')\in (FR)^\dagger$, such that $x_1\appr u$, $u'\appr x_1$, $v\appr x_2$, and $x_2\appr v'$. We can also use the symmetry of $R$, and then from $(x_1,x_2)\in R$ derive that there exist $(w,z),(w',z')$ such that $x_1\appr z$, $z'\appr x_1$, $w\appr x_2$, and $x_2\appr w'$. The situation can be illustrated as the following:
\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
		{u'} \&\& u \& v \&\& {v'} \\
		\& {x_1} \&\&\& {x_2} \\
		{z'} \&\& z \& w \&\& {w'}
		\arrow["\appr"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=1-4, to=2-5]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=2-2, to=3-3]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=1-6]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=2-5, to=3-6]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=3-1, to=2-2]
		\arrow["\appr"{marking, allow upside down}, draw=none, from=3-4, to=2-5]
	\end{tikzcd}
\end{equation*}

But then how can we derive $(x_1,x_2)\in (FR)^\dagger$?

\todo{Investigate more! Can it be doable really?!}
\subsection{Uniqueness of the witness in Hughes-Jacobs definition}
In this section we set $\rel$ to be the category that has sets as objects and binary relations as morphisms.
We answer the question that why there can be multiple simulation witnesses based on~\autoref{def:sim}, while for the same relation, there is only one witness according to Hughes-Jacobs simulation. 
 \begin{definition}[Hughes-Jacobs Simulation]
	For a functor $F$, and a poset $\appr$ over $F$ a HuJ-simulation is a relation $r$ for which there exists a morphism $\sigma\c r\to (Fr)^\dagger$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
	\begin{equation*}
		\begin{tikzcd}[ampersand replacement=\&]
			X \& R \& Y \\
			{FX} \& {\appr;(FR)^\dagger;\appr} \& {FY}
			\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["\beta", from=1-3, to=2-3]
			\arrow["{{Fp_1}_\appr}", from=2-2, to=2-1]
			\arrow["{{Fp_2}_\appr}"', from=2-2, to=2-3]
		\end{tikzcd}
	\end{equation*}
\end{definition}
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 \& Y\\
		{\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
		\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["\beta", from=1-3, to=2-3]
		\arrow["{{\powf p_1}_\subseteq}", from=2-2, to=2-1]
		\arrow["{{\powf 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),\beta(x_2))$.
But $\sigma'$ in the following diagram is not unique:
\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
		X \& R \& Y \\
		{\powf X} \& {(\powf R)^\dagger} \& {\powf Y}
		\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["\beta", from=1-3, to=2-3]
		\arrow["\subseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
		\arrow["{{\powf p_1^\dagger}}", from=2-2, to=2-1]
		\arrow["{{\powf 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(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ that $\sigma=\delta\comp\sigma'$, i.e., the following diagram commutes:
\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
		X \& R \& Y \\
		{\powf X} \& {(\powf R)^\dagger} \& {\powf Y} \\
		{\powf X} \& {\subseteq;(\powf R)^\dagger;\subseteq} \& {\powf Y}
		\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["\beta", 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["{{\powf p_1}_\subseteq}", from=3-2, to=3-1]
		\arrow["{{\powf p_2}_\subseteq}"', from=3-2, to=3-3]
	\end{tikzcd}
\end{equation*}
To define $\delta$, we define $c\c(\powf R^\dagger)\to((\powf R^\dagger)\times R)+(\powf R)^\dagger$ and $u\c((\powf R^\dagger)\times R)+(\powf R)^\dagger\to\subseteq;(\powf R)^\dagger;\subseteq$ and then we define $\delta=u\comp c$. Here are the definitions for $c$ and $u$:
\begin{gather*}
	c(w)=
	\begin{cases} 
		\inl(w,(x_1,x_2)) & \exists x_1,x_2, \sigma'(x_1,x_2)=w  \\
		\inr w & \mathsf{o.w}  
	\end{cases}\\
	u(\inl w,(x_1,x_2))=(\alpha(x_1),\alpha(x_2))\\
	u(\inr w)=w
\end{gather*}
\subsection{Symmetric simulation}
\begin{notation}
	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we show the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them.
\end{notation}
\begin{lemma}\label{lem:rel-span-equiv}
	$r\c X\rto Y$ is a morphism in $\rel$ iff there is an object $(r,p_1,p_2)$ in $\spa$.
\end{lemma}
\begin{proof}
	($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$.
	
	($\Leftarrow$): If $(r,p_1,p_2)$ is an object in $\spa$, then $r$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rel$.\qed
\end{proof}
The above translation seems to be true in a more general case, where $\spa$ and $\rel$ are defined on an arbitrary category (the latter is called an allegory then).
\begin{definition}[Relator]
	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$. 
\end{definition}
 
\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim}
	For a relator $\relar$ on a functor $F$ a HJ-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
	\begin{equation}\label{eq:hej-sim}
		\begin{tikzcd}[ampersand replacement=\&]
			X \& r \& Y \\
			{FX} \& {\relar r} \& {FY}
			\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["\beta", from=1-3, to=2-3]
			\arrow["{{(Fp_1)}^\relar}", from=2-2, to=2-1]
			\arrow["{{(Fp_2)}^\relar}"', from=2-2, to=2-3]
		\end{tikzcd}
	\end{equation}
\end{definition}

\begin{definition}[Relator-based Simulation]
	Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$,	i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
\end{definition}

\begin{definition}[Symmetric Relator]
	A relator $\relar$ is symmetric if and only if for every relation $r$ we have $\relar(r^\op)=(\relar r)^\op$.
\end{definition}

\begin{definition}[Relator-based Bisimulation]
	Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r$ is a $\relar$-simulation, and $\relar$ is a symmetric relator.
\end{definition}

\begin{notation}
	From now on we refer to relator-based simulations of a relator $\relar$ with $\relar$-simulation. If we talk about a HJ-simulation we specify the witness.
\end{notation}

\begin{lemma}\label{lem:sim-simp}
	$r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. 
\end{lemma}
\begin{proof}
	$r$ being a $\relar$-simulation means $r\leq\beta^\op\comp\relar r\comp\alpha$, meaning that if $x\;r\;y$ then $x \;\alpha;\relar r;\beta^\op\; y$, and it means that there exist $w\in\relar r$ that its first element is equal with $\alpha(x)$ and its second element is equal with $\beta(y)$, enabling us to say $\alpha(x)\;\relar r\; \beta(y)$.\qed
\end{proof}

\begin{prop}
	For a relator $\relar$ of a functor $F$, a relation $r$ is a $\relar$-simulation from $\alpha\c X\to FX$ to $\beta\c Y\to FY$ iff it is a HJ-simulation with the witness $\sigma\c r\to\relar r$.
\end{prop}
\begin{proof}
	($\Rightarrow$): $r$ being a $\relar$-simulation means that $x\;r\;y$ gives $\alpha(x)\;\relar r\;\beta(y)$. Since $r$ and $\relar r$ are both relations, by~\autoref{lem:rel-span-equiv} there exist objects $(r,p_1,p_2)$ and $(\relar r,(Fp_1)^\relar,(Fp_2)^\relar)$ in $\spa$. We define $\sigma\c r\to\relar r$ to be $\sigma(x,y)=(\alpha(x),\beta(y))$. $\sigma$ commutes in~\eqref{eq:hej-sim}, so we have a HJ-simulation.
	
	($\Leftarrow$): Assuming we have a $\sigma$ that commutes in~\eqref{eq:hej-sim}, we want to prove that if $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. By~\eqref{eq:hej-sim} we have $\alpha\comp p_1=(Fp_1)^\relar\comp\sigma$ and $\alpha\comp p_2=(Fp_2)^\relar\comp\sigma$. It means that since $x\;r\;y$ then exists $w\in\relar r$, such that $\sigma(x,y)=w$, where $(Fp_1)^\relar(w)=\alpha(x)$ and $(Fp_2)^\relar(w)=\beta(y)$. So, we have $\alpha(x) \;\relar r \;\beta(y)$.\qed
\end{proof}
\begin{prop}
	For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique.
\end{prop}
\begin{proof}
	It only relies on the fact that ${(Fp_1)}^\relar$ and ${(Fp_2)}^\relar$ in~\eqref{def:hej-sim} are jointly monic.\qed
\end{proof}
\begin{definition}
	We call $\hat{\relar}$ a symmetrization of a relator $\relar$ iff for a relation $r$ it is defined as follows:
	\begin{gather*}
		\hat{\relar}r=\relar r\cap (\relar(r^\op))^\op
	\end{gather*}
\end{definition}
\begin{prop}
	For every relator $\relar$, $\hat{\relar}$ is a relator.
\end{prop}
\begin{proof}
	Almost obvious!\qed  
\end{proof}
\begin{prop}
	Assuming that $\relar$ is a relator, and $r$ and $r^\op$ are both $\relar$-simulations from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ and vice-versa respectively, then $r$ is also a $\hat{\relar}$-simulation.
\end{prop}
\begin{proof}
	We need to prove that $x\; r\;y$ gives $\alpha(x)\;\hat{\relar} r\;\beta(y)$.
	 $r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. So, we are left to prove $\alpha(x)\;(\relar (r^\op))^\op\;\beta(y)$. $x\;r\;y$ gives $y\;r^\op\;x$, and $r^\op$ being a $\relar$-simulation from $\beta$ to $\alpha$ gives $\beta(y)\;\relar r^\op\; \alpha(x)$. So, we have $\alpha(x) \;(\relar(r^\op))^\op \;\beta(y)$. \qed
\end{proof}
\begin{cor}
	Assuming that $\relar$ is a relator, and $r$ is a symmetric $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to itself, then $r$ is also a $\hat{\relar}$-simulation.
\end{cor}
\begin{remark}
	If we want to have the previous corollary for two different coalgebras $\alpha\c X\to FX$ and $\beta\c X\to FX$, we need to assume that $r^\op$ is also a $\relar$-simulation from $\beta$ to $\alpha$. 
\end{remark}

\begin{prop}
	$\hat{\relar}$ is a symmetric relator, i.e., every $\hat{\relar}$-simulation is actually a $\hat{\relar}$-bisimulation.
\end{prop}
\begin{proof}
	\begin{align*}
		\hat{\relar}(r^\op)&\\
		&=\relar(r^\op)\cap(\relar (r^\op)^\op)^\op\\
		&=\relar(r^\op)\cap(\relar r)^\op\\
		&=(\relar r)^\op\cap\relar(r^\op)\\
		&=(((\relar r)^\op\cap\relar(r^\op))^\op)^\op\\
		&=(\relar r\cap(\relar(r^\op))^\op)^\op\\
		&=(\hat{\relar}r)^\op
	\end{align*}\qed
\end{proof}

\begin{prop}
	Assuming that $\relar$ is a symmetric relator, and $r$ is a $\relar$-simulation from a coalgebra $(X,\alpha)$ to itself, then $r^\op_{s}$ is a $\relar$-simulation as well.
\end{prop}
\begin{proof}
	It is easy to directly show that $r^\op$ is a $\relar$-simulation.\qed
\end{proof}
\begin{cor}
		Assuming that $\relar$ is a symmetric relator, then the $\relar$-simularity from a coalgebra $(X,\alpha)$ to itself is a symmetric relation.
\end{cor}

\begin{prop}
	Assuming that $\relar$ is a symmetric relator, then for every $r$ that is a $\relar$-simulation, $r^\op$ is also a $\relar$-simulation. 
\end{prop}
\begin{proof}
	Assuming $y\; r^\op x$ we have $x\; r\; y$. Since $r$ is $\relar$-simulation we have $\alpha(x)\;\relar r\;\beta (y)$. So, we have $\beta(y)\;(\relar r)^\op\;\alpha(x)$, and since $\relar$ is symmetric we have $\beta(y)\;\relar r^\op\;\alpha(x)$.\qed
\end{proof}

\begin{definition}[Behavioural Equivalence]
	Two states $x$ and $y$ of two coalgebras $(X,\alpha)$ and $(Y,\beta)$ are behaviourally equivalent iff there exist a coalgebra $(Z,\gamma)$ and coalgebra morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ such that $f(x)=g(y)$. The relation $r$ consisting of all behaviourally equivalent states of these two coalgebras is called behavioural equivalence.
\end{definition}

\begin{definition}[Difunctional Relation]
	A relation $r\c X\rto Y$ is difunctional iff there are functions $f\c X\to Z$ and $g\c Y\to Z$ such that for every $(x,y)\in R$ we have $f(x)=g(y)$.
\end{definition}

\begin{definition}[Soundness and Completeness of $\relar$-similarity]
	For a relator $\relar$ the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is sound iff it is less than or equal to their behavioural equivalence, and it is complete iff it is greater than or equal to their behavioural equivalence.
\end{definition}

\begin{thm}
	Let $\relar$ be a relator for a functor $F$:
	\begin{enumerate}
		\item If for all functions $f\c X\to A$ and $g\c Y\to A$, $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\relar$-similarity is complete.
		\item If $\relar$ preserves difunctional relations and for every epi-cospan $(f\c X\to A,g\c Y\to A)\in\Set$, $\relar(g^\op\comp f)\leq(Fg)^\op\comp Ff$, then $\relar$-similarity is sound.
	\end{enumerate}\qed
\end{thm}

\begin{prop}\label{prop:difunc-preser}
	Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, then $\hat{\relar}$ does the same.
\end{prop}
\begin{proof}
	Assuming $r$ is difunctional, then there exist $f_1,f_2\c FX\to FZ$ and $g_1,g_2\c FY\to FZ$ such that $p\;\relar r\;q$ iff $f_1(p)=g_1(q)$ and $q \;\relar r^\op \;p$ iff $f_2(p)=g_2(q)$. By the definition of $\hat{\relar}$ we have $p\;\hat{\relar}r\;q$ iff $p\;\relar r\;q$ and $p\;(\relar r^\op)^\op\;q$ that is equivalent to say that $\brks{f_1,f_2}(p)=\brks{g_1,g_2}(q)$.\qed
\end{proof}
\begin{cor}
	Assuming that $\relar$ is a $F$-relator that preserves difunctional relations, for every symmetric relation $r$ we have $\hat{\relar}r=\relar r$.
\end{cor}
\begin{proof}
	$\relar$-similarity being symmetric means that for the $f_1$, $f_2$, $g_1$ and $g_2$ in the proof of~\autoref{prop:difunc-preser}, we have $f_1=f_2$ and $g_1=g_2$.\qed
\end{proof}

Assuming that $\relar$-similarity is complete, does not guarantee that $\hat{\relar}$-similarity is sound and complete. We give a counter-example. Assuming that $\relar$ is a $\powf$-relator that takes $r\c X\rto Y$ to $\powf X\times \powf Y$, then $\hat{\relar} r= \powf X\times\powf Y$ as well. It means that for every coalgebras $(X,\alpha)$, $(Y,\beta)$, $\hat{\relar}$-similarity is equal to $X\times Y$, which is rare to be equal to behavioural equivalence. For example, if we take $X=\{x_1,x_2\}$ and $Y=\{y_1,y_2,y_3\}$, and we define $\alpha$ and $\beta$ as 
\begin{gather*}
	\alpha(x)=
	\begin{cases} 
		\{x_1,x_2\} & x=x_1  \\
		\{x_2\} & x=x_2
	\end{cases}
	\intertext{and}
	\beta(y)=
	\begin{cases} 
		\{y_3\} & y=y_1  \\
		Y & y=y_2\\
		\emptyset & y=y_3
	\end{cases}
\end{gather*}
then at least $(x_1,y_3)$ is not in the behavioural equivalence, while it is in $\hat{\relar}$-similarity.

\begin{prop}
	Assuming that $\relar$-similarity is symmetric and complete, then $\hat{\relar}$-similarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete.
\end{prop}
\begin{proof}
	(Completeness): We show $\relar$-similarity with $r_s$ and $\hat{\relar}$-similarity with $r_{\hat{s}}$. Also, we show the behabioural equivalence with $r_b$. Since  
\end{proof}

\begin{prop}
	Assuming that $\relar$ is a $F$-relator ($F$ is a set functor), that for every functions $f\c X\to Z$ and $g\c Y\to Z$, we have $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\hat{\relar}$-similarity is complete.
\end{prop}
\begin{proof}
	We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$ we have $\hat{\relar}(g^\op\comp f)\geq (Fg)^\op\comp Ff$. By the assumption we have $\relar(g^\op\comp f)\geq(Fg)^\op\comp Ff$. Also, again from the assumption we have $\relar(f^\op\comp g)\geq(Ff)^\op\comp Fg$ that gives $(\relar(f^\op\comp g))^\op\geq(Fg)^\op\comp Ff$. So, we have $\hat{\relar}(g^\op\comp f)\geq F(g)^\op\comp Ff$.\qed
\end{proof}
\begin{prop}
	Assuming that $\relar$ is a symmetric relator for a functor $F\c\Set\to\Set$, then the $\relar$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound, using the axiom of choice.
\end{prop}
\begin{proof}
	We call the bisimilarity relation $r$, and we assume $x_1\;r\;x_2$, now we need to prove that $x_1$ and $x_2$ are behaviourally equivalent. We take $Z=X/r$, where $X/r=\{[x]\mid [x]=\{y\mid x\;r\;y\}\}$. Now, we define the coalgebra homomorphism $f\c X\to X/r$ as $f(x)=[x]$. So, assuming $x_1\;r\;x_2$ gives $f(x_1)=f(x_2)$. Now, assuming that exists a choice function $c\c X/r\to X$ that $c\comp f=\id_X$, we define $\gamma\c X/r\to F(X/r)$, as $\gamma([x])=Ff\comp\alpha\comp c([x])$. Now, we have
	\begin{align*}
		\gamma\comp f&\\
		&=Ff\comp\alpha\comp c\comp f\\
		&=Ff\comp\alpha.
	\end{align*}
	So, $x_1$ and $x_2$ are behaviourally equivalent. So, the $\relar$-bisimilarity is sound.\qed
\end{proof}
\begin{cor}
	Assuming that a relator $\relar$ over a functor $F\c\Set\to\Set$ satisfies $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$ for every functions $f\c X\to Z$ and $g\c Y\to Z$, then $\hat{\relar}$-bisimilarity from a coalgebra $\alpha\c X\to FX$ to itself is sound and complete, using the axiom of choice.
\end{cor}
\subsection{Egli-Milner relator and Barr relators}
\begin{definition}
	We call the map $\emre\c\rel\to\rel$ the Egli-Milner $\powf$-relator, whenever for every relation $r\c X\rto Y$ it is defined as follows:
	\begin{gather*}
		\emre r=\{(S,T)\mid x\in S\Rightarrow \exists y\in T, x\;r\;y\}
	\end{gather*}
\end{definition}
Egli-Milner relator is not sound or complete, although its symmetrization is sound and complete.
\begin{prop}
	$\hat{\emre}$-similarity from a coalgebra $(\alpha,X)$ to $(\beta,Y)$ is sound and complete.
\end{prop}
\begin{proof}
	We need to prove that for every functions $f\c X\to Z$ and $g\c Y\to Z$, $\hat{\emre}(g^\op\comp f)=(\powf g)^\op\comp\powf f$. 
	We have $S\;\hat{\emre}(g^\op\comp f)\;T$ iff $S\;\emre(g^\op\comp f)\;T$ and $T\;\emre(f^\op\comp g)\;S$. Then we have
	\begin{align*}
		S\;\emre(g^\op\comp f)\;T&\\
		&\iff\forall x\in S,\exists y\in T, x\;g^\op\comp f\; y\\
		&\iff \forall x\in S,\exists y\in T,z\in Z, x\;f\;z\; , \; y\;g\;z,
	\end{align*}
	and
	\begin{align*}
		T\;\emre(f^\op\comp g)\;S&\\
		&\iff\forall y\in T,\exists x\in S, y\;f^\op\comp g\; x\\
		&\iff \forall y\in T,\exists x\in S, z\in Z, x\;f\;z\; , \; y\;g\;z.
	\end{align*}
	It is equivalent with the following:
	\begin{gather*}
		\forall x\in S,\exists y\in T, f(x)=g(y),\\
		\forall y\in T,\exists x\in S, f(x)=g(y).
	\end{gather*}
	Equivalently, $Im(f\mid_S)=Im(g\mid_T)$, and we call images $U$ that is in $\powf Z$. So, we equivalently have
	\begin{align*}
		S\;\powf f\;U,\; T\;\powf g\;U&\\
		&\iff S\;\powf f\;U,\; U\;(\powf g)^\op\;T\\
		&\iff S\;(\powf g)^\op\comp\powf f\;T
	\end{align*}\qed
\end{proof}
For every relation $r\rto X\to Y$ $\emre r=\subseteq\;\emre r=\emre r\;\subseteq=\subseteq;\emre r;\subseteq$.
%\begin{prop}
%	Assuming that $r\c X\rto Y$, then $\subseteq;\hat{\emre}r;\subseteq=\subseteq;\hat{\emre}r$ and $\subseteq;\hat{\emre}r=\hat{\emre}r;\subseteq$.
%\end{prop}


Barr relator is a generalization of the Egli-Milner relator, where the functor is generalized.

\begin{definition}[Barr relator]
	A relator over a functor $F$ is a Barr relator, shown by $\bar{F}$, iff for a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
	\begin{gather*}
		\bar{F}r=F\pi_2\comp(F\pi_1)^\op
	\end{gather*}
\end{definition}
\begin{prop}
	For every set-functor $F$, the barr relator $\bar{F}$ is symmetric.
\end{prop}
\begin{proof}
	Assuming that for a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ we have $r=\pi_2\comp\pi_1^\op$, then we have:
	\begin{align*}
		\hat{\bar{F}}r&\\
		=&\bar{F}r\cap(\bar{F}r^\op)^\op\\
		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_2\comp\pi_1^\op)^\op)^\op\\
		=&\bar{F}(\pi_2\comp\pi_1^\op)\cap(\bar{F}(\pi_1\comp\pi_2^\op))^\op\\
		=&F\pi_2\comp(F\pi_1)^\op\cap(F\pi_1\comp (F\pi_2)^\op)^\op\\
		=&F\pi_2\comp(F\pi_1)^\op\cap F\pi_2\comp (F\pi_1)^\op\\
		=&F\pi_2\comp(F\pi_1)^\op\\
		=&\bar{F}r
	\end{align*}\qed
\end{proof}
\begin{prop}
	$\hat{L}$ is a Barr relator.
\end{prop}
\begin{proof}
	\todo{Finish.}
\end{proof}

\begin{definition}[Mid-lax Barr relator]
	Given a relation $r$, and take a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$. Assuming that $\appr$ is a partial order over a functor $F$, then the relator over $F$ and shown with $\overrightarrow{F}$ is a \emph{mid-lax Barr relator} if we have:
%	A relator over a functor $F$ is a one-sided Barr relator, shown by $\overrightarrow{F}$, iff for a partial order $\appr$ over $F$, a relation $r\c X\rto Y$, and a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ that $r=\pi_2\comp\pi_1^\op$ we have:
	\begin{gather*}
		\overrightarrow{F}r=F\pi_2\comp\appr\comp(F\pi_1)^\op
	\end{gather*}
\end{definition}

\begin{prop}
	For every functor $F\c\Set\to\Set$, the symmetrization of the mid-lax Bar relator is equal with the Barr relator.
\end{prop}
\begin{proof}
%	Where there exist $\pi_1\c A\to X$ and $\pi_2\c A\to Y$ such that $r=\pi_2\comp\pi_1^\op$, we assume that $s \;\hat{\overrightarrow{F}}r\; t$, and we need to show that $s\;F\pi_2\comp(F\pi_1)^\op\;t$. Considering that $r^\op=\pi_1\comp\pi_2^\op$, we have:
%	\begin{align*}
%		s \;\hat{\overrightarrow{F}}r\; t&\\
%		&\iff s\;\overrightarrow{F}r\;t\qquad\&\qquad s \;(\overrightarrow{F}r^\op)^\op\; t\\
%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;(F\pi_1\comp\appr\comp(F\pi_2)^\op)^\op\;t\\
%		&\iff s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t \qquad\&\qquad s\;F\pi_2\comp\appr\comp(F\pi_1)^\op\;t
%	\end{align*}
%	Since $F\pi_1$ is a surjective function, then exists at least one $w\in FA$ such that $(F\pi_1)^\op(s)=w$, and:
%	\begin{gather*}
%		w\;F\pi_2\comp\appr\; t \qquad\&\qquad w\;F\pi_2\comp\appr\; t
%	\end{gather*}
%	And similarly, since $F\pi_2$ is also a surjective function we have at least one $v\in FA$ such that $(F\pi_2^\op)(t)=v$, and:
%	\begin{align*}
%		&w\;\appr\; v \qquad\&\qquad w\;\appr\; v\\
%		\iff&(F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t) \qquad\&\qquad (F\pi_1)^\op(s)\;\appr\; (F\pi_2^\op)(t)\\
%		\iff&(F\pi_1)^\op(s)\;=\; (F\pi_2^\op)(t)\\
%		\iff&s\; F\pi_2\comp(F\pi_1)^\op\;t\\
%		\iff&s\;\bar{F}r\;t
%	\end{align*}
%	So we have $\hat{\overrightarrow{F}}\leq \bar{F}$.
%	Now, we are left to show that $\bar{F}\leq\hat{\overrightarrow{F}}$. For that, reading the given proof from the end to the starting point is sufficient.
\todo{Finish.}
\end{proof}

\begin{prop}
	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$ the following propositions hold:
	\begin{enumerate}
		\item $\powf\pi_2\comp\subseteq\comp(\powf\pi_1)^\op\quad=\quad\subseteq\comp \powf\pi_2\comp(\powf\pi_1)^\op$
		\item $\powf\pi_1\comp\subseteq\comp(\powf\pi_2)^\op\quad=\quad\subseteq\comp \powf\pi_1\comp(\powf\pi_2)^\op$
	\end{enumerate}
\end{prop}
\begin{proof}
	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op\quad=\quad\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op$.
	
	Assuming $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$, then exist $z$ and $z'$ such that
	\begin{gather*}
		z \mathrel{(\powf\pi_i)} x,\\
		z \mathrel{\subseteq} z',\\
		z'\mathrel{(\powf\pi_j)} y.
	\end{gather*}
	Then from $z \mathrel{\subseteq} z'$ we get $\powf\pi_j(z)\mathrel{\subseteq}y$. So, we have $z\mathrel{\subseteq\comp \powf\pi_j} y$, thus $x\mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$.
	
	Now, assuming $x \mathrel{\subseteq\comp \powf\pi_j\comp(\powf\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
	\begin{gather*}
		z\mathrel{(\powf\pi_i)} x,\\
		z \mathrel{(\powf\pi_j)} y',\\
		y' \mathrel{\subseteq} y.
	\end{gather*}
	We take the set $w=z\cup (\powf\pi_i(z)\times y)$ for which we have $z\subseteq w$ and $\powf\pi_j(w)=y$. So, we have $w \mathrel{(\powf\pi_j)} y$,  $z\mathrel{\subseteq} w$, and $z\mathrel{(\powf\pi_i)} x$ that gives $x \mathrel{\powf\pi_j\comp\subseteq\comp(\powf\pi_i)^\op} y$.\qed
\end{proof}
	
%\begin{lemma}
%	Assuming that $F\pi_1$ and $F\pi_2$ are monotone with respect to $\sqsubseteq$ that is an order over $F$, then the following propositions hold:
%	\begin{enumerate}
%		\item $F\pi_2\comp\sqsupseteq\comp(F\pi_1)^\op\quad=\quad\sqsupseteq\comp F\pi_2\comp(F\pi_1)^\op$
%		\item $F\pi_1\comp\sqsupseteq\comp(F\pi_2)^\op\quad=\quad\sqsupseteq\comp F\pi_1\comp(F\pi_2)^\op$
%	\end{enumerate}
%\end{lemma}
%\begin{proof}
%	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op\quad=\quad\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op$.
%	
%	Assuming $x \mathrel{F\pi_j\comp\sqsupseteq\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
%	\begin{gather*}
%		z \mathrel{(F\pi_i)} x,\\
%		z \mathrel{\sqsubseteq} z',\\
%		z'\mathrel{(F\pi_j)} y.
%	\end{gather*}
%	Then from $z \mathrel{\sqsubseteq} z'$ we get $F\pi_j(z)\mathrel{\sqsubseteq}y$. So, we have $z\mathrel{\sqsupseteq\comp F\pi_j} y$, thus $x\mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$.
%	
%	Now, assuming $x \mathrel{\sqsupseteq\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
%	\begin{gather*}
%		z\mathrel{(F\pi_i)} x,\\
%		z \mathrel{(F\pi_j)} y',\\
%		y' \mathrel{\sqsubseteq} y.
%	\end{gather*}
%\end{proof}
\begin{prop}
	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ is either the maybe monad, the subdistribution monad or $FX=\powf(X\times A)$, where $A$ is a set of labels, then the following propositions hold:
	\begin{enumerate}
		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
	\end{enumerate}
\end{prop}
\begin{proof}
	\todo{Finish.}
\end{proof}
\begin{definition}[Natural Order Structure]\label{def:nat-ord}
	A \emph{natural order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ such that if $\alpha\appr\beta$ in $\Hom(X,FY)$, $f\c X'\to X$, $g\c Y\to Y'$, then:
	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
		\item $\alpha\comp f\appr\beta\comp f$ in $\Hom(X',FY)$. \label{item:nat-ord:I}
		\item $Fg\comp\alpha\appr Fg\comp\beta$ in $\Hom(X,FY')$. \label{item:nat-ord:II}
	\end{enumerate}
\end{definition}
\begin{prop}
	In $\Set$, assuming that $Ff\comp g\appr h$ where $g,h\in\Hom(1,FY)$, generalizes to the case where $g,h\in\Hom(X,FY)$, where $X$ is an arbitrary set.  
\end{prop}
\begin{proof}
	We assume that for every set $Y$ we have a preorder structure on $\Hom(1,FY)$. 
	\todo{Prove it and then edit the examples accordingly!}
\end{proof}
\begin{definition}[Good Order Structure]\label{def:good-ord}
	A \emph{good order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $h\appr  Fg\comp k$ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k'\appr k$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}
\begin{definition}[Cogood Order Structure]\label{def:cogood-ord}
	A \emph{cogood order structure} on a functor $F$ is a preorder $\appr$ on each Hom-set of the form $\Hom(X,FY)$ that is a natural order structure, and if $h\c X\to FZ$, $k\c X\to FY$, $g\c Y\to Z$, $Fg\comp k\appr h $ in $\Hom(X,FZ)$, then there is $k'\c X\to FY$ such that $k\appr k'$ in $\Hom(X,FY)$ and $h=Fg\comp k'$.
\end{definition}

\begin{lemma}\label{lem:good}
	Assuming that a a functor $F$ has an order structure $\appr$ that is good, then for every $f\in\Hom(X,FY)$ we have:
	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
		\item $Ff\comp\sappr\quad=\quad\sappr\comp Ff$
		\item $(Ff)^\op\comp\appr\quad=\quad\appr\comp (Ff)^\op$
	\end{enumerate}
\end{lemma}
\begin{proof}
	$(I)$ Assuming $t\mathrel{Ff\comp\sappr} x$\footnote{add parenthesis}, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is good, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{\sappr\comp Ff} x$.
	
	Assuming $t\mathrel{\sappr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:good-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.
	
	$(II)$ Basically, by definition of $\op$ and relation composition we have
	\begin{gather*}
		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
	\end{gather*}
	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
\end{proof}
\begin{lemma}\label{lem:cogood}
	Assuming that a a functor $F$ has an order structure $\appr$ that is cogood, then for every $f\in\Hom(X,FY)$ we have:
	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
		\item $Ff\comp\appr\quad=\quad\appr\comp Ff$
		\item $(Ff)^\op\comp\sappr\quad=\quad\sappr\comp (Ff)^\op$
	\end{enumerate}
\end{lemma}
\begin{proof}
	$(I)$ Assuming $t\mathrel{Ff\comp\appr} x$, there exists $s$ such that $t\appr s$ and $Ff(s)=x$. Since $\appr$ is cogood, and thus natural, by~\autoref{def:nat-ord}, from $t\appr s$ we get $Ff(t)\appr x$ that is $t\mathrel{\appr\comp Ff} x$.
	
	Assuming $t\mathrel{\appr\comp Ff} x$, there exists $y$ such that $Ff(t)=y$ and $y\appr x$. By~\autoref{def:cogood-ord} since $Ff(t)\appr x$ there exists $s$ that $t\appr s$ and $Ff(s)=x$ that is $t\mathrel{Ff\comp\appr}s$.
	
	$(II)$ Basically, by definition of $\op$ and relation composition we have
	\begin{gather*}
		(Ff\comp\appr)^\op=\sappr\comp(Ff)^\op,\\
		(\appr\comp Ff)^\op=(Ff)^\op\comp\sappr.
	\end{gather*}
	So it follows directly from applying $\op$ on both sides of $(I)$.\qed 
\end{proof}
%\begin{prop}
%	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has a cogood order structure $\appr$, the following propositions hold:
%	\begin{enumerate}
%		\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad\appr\comp F\pi_2\comp(F\pi_1)^\op$
%		\item $F\pi_1\comp\appr\comp(F\pi_2)^\op\quad=\quad\appr\comp F\pi_1\comp(F\pi_2)^\op$
%	\end{enumerate}
%\end{prop}
%\begin{proof}
%	Without loss of generality, we assume $i,j\in\{1,2\}$, and $i\neq j$, and prove $F\pi_j\comp\appr\comp(F\pi_i)^\op\quad=\quad\appr\comp F\pi_j\comp(F\pi_i)^\op$.
%	
%	Assuming $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$, then exist $z$ and $z'$ such that
%	\begin{gather*}
%		z \mathrel{(F\pi_i)} x,\\
%		z \mathrel{\appr} z',\\
%		z'\mathrel{(F\pi_j)} y.
%	\end{gather*}
%	Then from $z \mathrel{\appr} z'$ since $\appr$ is a cogood order structure by~\ref{item:nat-ord:I} we get $F\pi_j(z)\mathrel{\appr}y$. So, we have $z\mathrel{\appr\comp F\pi_j} y$, thus $x\mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$.
%	
%	Now, assuming $x \mathrel{\appr\comp F\pi_j\comp(F\pi_i)^\op} y$, then there exist $z$ and $y'$ such that
%	\begin{gather*}
%		z\mathrel{(F\pi_i)} x,\\
%		z \mathrel{(F\pi_j)} y',\\
%		y' \mathrel{\appr} y.
%	\end{gather*}
%	Since $\appr$ is a cogood order structure by~\autoref{def:cogood-ord} there exists a $w$ such that  $z\appr w$ and $F\pi_j(w)=y$. So, we have $w \mathrel{(F\pi_j)} y$,  $z\mathrel{\appr} w$, and $z\mathrel{(F\pi_i)} x$ that gives $x \mathrel{F\pi_j\comp\appr\comp(F\pi_i)^\op} y$.\qed
%\end{proof}
\begin{prop}
	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that $F$ has an order structure $\appr$, the following propositions hold:
	\begin{enumerate}
		\item If $\appr$ is good, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad F\pi_2\comp(F\pi_1)^\op\comp\appr$
		\item If $\appr$ is cogood, we have $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad=\quad \appr\comp F\pi_2\comp(F\pi_1)^\op$
		\item If $\appr$ is both good and cogood, all the following are equal:
		\begin{itemize}
			\item $F\pi_2\comp\appr\comp(F\pi_1)^\op\quad$
			\item $F\pi_2\comp(F\pi_1)^\op\comp\appr$
			\item $\appr\comp F\pi_2\comp(F\pi_1)^\op$
			\item $\appr\comp F\pi_2\comp(F\pi_1)^\op\comp\appr$
		\end{itemize}
	\end{enumerate}
\end{prop}
\begin{proof}
	They all follow in an obvious way from~\autoref{lem:good} and~\autoref{lem:cogood}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed
\end{proof}
\begin{example}
	In the category of sets, subset over the powerset functor is an example of a good order. For every $h\c X\to\powf Z$, $k\c X\to \powf Y$, and $g\c Y\to Z$, such that $h\subseteq\powf g\comp k$, we define $k'\c X\to\powf Y$ that for every $x\in X$, $k'(x)=k(x)\setminus\{y\mid g(y)\notin h(x)\}$\footnote{Change to $\{y\mid g(y)\in h(x)\}$}. We show that for every $x\in X$, we have $\powf g\comp k'(x)=h(x)$.
	
	Assuming $z\in\powf g(k'(x))$, then there exists $y'\in k(x)\setminus \{y\mid g(y)\notin h(x)\}$ that $g(y')=z$, so $y'\in k(x)$, $y'\notin\{y\mid g(y)\notin h(x)\}$. $y'\notin\{y\mid g(y)\notin h(x)\}$ means that $g(y')\in h(x)$, thus $\powf g\comp k'\subseteq h$.
	
	Assuming $z\in h(x)$, since $h\subseteq \powf g\comp k$, then $z\in\powf g\comp k(x)$. So, there exists $y'$ such that $y'\in k(x)$ and $g(y')=z$. Since $g(y')\in h(x)$ then $y'\notin\{y\mid g(y)\notin h(x)\}$ meaning that $y'\in k'(x)$ that means $z\in \powf g(k'(x))$, thus $h\subseteq \powf g\comp k'$.\qed
\end{example}
\begin{example}
	In the category of sets, subset over the powerset functor is NOT an example of a cogood order! For some set $X$ we take $h\c X\to\powf\mathbb{Z}$, for every $x\in X$, $h(x)=\mathbb{Z}$, $g\c\mathbb{Z}\to\mathbb{Z}$, and for every $z\in\mathbb{Z}$, 
	\begin{gather*}
		g(z)=
		\begin{cases} 
			0 & z\in\mathbb{Z}^+ \\
			1 & \mathsf{otherwise}  
		\end{cases}
	\end{gather*}
	then 
	\begin{gather*}
		\powf g(A)=
		\begin{cases} 
			\emptyset & A=\emptyset \\
			\{0\} & A\subseteq \mathbb{Z}^+,A\neq\emptyset\\  
			\{1\} & A\subseteq \mathbb{Z}^-\cup\{0\},A\neq\emptyset\\
			\{0,1\} & \mathsf{otherwise} 
		\end{cases}
	\end{gather*}
	then no matter what $k\c X\to\powf\mathbb{Z}$ is there will be no $k'\c X\to\powf\mathbb{Z}$, for every $x\in X$, $\powf g(k'(x))=h(x)$, as $\powf g(k'(x))\subseteq\{0,1\}$, while $h(x)=\mathbb{Z}$, so $\powf g(k'(x))\subset h(x)$.
\end{example}
The previous example suggests that cogoodness is a strong condition. Perhaps it can be limited to be meaningful. Maybe the morphism $g$ can be limited to legs of a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, where for a relation $r$, $r=\pi_2\comp\pi_1^\op$.\footnote{Or maybe because the $g$ in the counter-example is not surjective!}
\begin{prop}
	For a natural order structure $\appr$ on a set-functor $F$, if for every $f\in\Hom(X,FY)$ we have $Ff\comp\appr=\appr\comp Ff$, then $\appr$ is cogood.
\end{prop}
\begin{proof}
	\todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a good order structure forces every witness for AM-simulation to have the left cell of the lax diagram as equality, and subset on powerset functor is a good order structure, then what is the counter-example number 4 that you have?!}
\end{proof}
\begin{prop}
	Assuming that $\relar$ is a difunctionally functorial relator, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\relar r\comp\appr$ is a sound relator. 
\end{prop}
\begin{proof}
	\todo{Finish.}
\end{proof}
\begin{prop}
	Assuming that $\relar$ is a relator over $F\c\Set\to\Set$, and $\appr_{X}$ and $\appr_{Y}$ are posets over $FX$ and $FY$ respectively, then the symmetrization of the relator that takes $r\c X\rto Y$ to $\appr_{X};\relar r;\appr_{Y}$ is a Barr relator.
\end{prop}
\begin{proof}
	\todo{Finish.}
\end{proof}
\end{document}














