\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{\spto}{\mathrel{\tikz{\draw[-{Stealth}] (0.0,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);}}}
\newcommand{\rto}{\mathrel{\tikz{\draw[-{Stealth}] (0.04,0) -- (0.4,0); \draw (0.17,0.07) -- (0.17,-0.07);\draw (0.04,0) -- (0,-0.07);\draw (0.04,0) -- (0,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{Relation Lifting}
\begin{definition}[Natural Order Structure]\label{def:nat-ord}
	A \emph{natural order structure} on a functor $F$ is a poset $\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}
We want to say that a natural order structure entails an order over a functor defined by Jacobs and Hughes that is a functor of the type $\Set\to\mathbf{Poset}$.
\begin{prop}
	Assuming that $F\c\Set\to\Set$ is a functor, and we have a natural order structure on $F$, then we have a functor $\tilde{F}\c\Set\to\mathbf{Poset}$, such that $U\comp \tilde{F}=F$, where $U$ is a forgetful functor.
\end{prop}
\begin{proof}
	We take $\tilde{F}X=\Hom(1,FX)$. Assuming that $U$ takes every poset to its carrier set, then we have $U\comp\tilde{F}X=FX$ for every object $X$.\qed
\end{proof}
\section{Coalgebraic Bisimulation}%\label{sec:}
In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
such spans $(X \stackrel{p_1}{\leftarrow} R
\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono.
We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$
($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ 
in $\BC$ that the following diagram commutes:
	\begin{equation*}
		\begin{tikzcd}[ampersand replacement=\&]
			{X_1} \& R \& {X_2} \\
			{Y_1} \& S \& {Y_2}
			\arrow["{g_1}"', from=1-1, to=2-1]
			\arrow["{{p_1}}"', from=1-2, to=1-1]
			\arrow["{{p_2}}", from=1-2, to=1-3]
			\arrow["f", from=1-2, to=2-2]
			\arrow["{g_2}", from=1-3, to=2-3]
			\arrow["{q_1}", from=2-2, to=2-1]
			\arrow["{q_2}"', from=2-2, to=2-3]
		\end{tikzcd}
	\end{equation*}

\begin{definition}[Relation Lifting]
	Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
	\begin{equation*}
		\begin{tikzcd}[ampersand replacement=\&]
			\rel(\BC) \&\& \rel(\BC) \\
			{\BC\times\BC} \&\& {\BC\times\BC}
			\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 have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained 
by the image factorization in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
%
%\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 define a functor of type $(-)^\dagger\c\spa(\BC)\to\rel(\BC)$. It takes every span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the image of its legs:

\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
			R \& {R^\dagger} \&\& {X\times Y}
			\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*}

So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to the following relation:
\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
		\& {(FR)^\dagger} \& \\
		FX \&\& FY \\
		\& {FX\times FY}
		\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*}
%
%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. 
For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly.

We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us 
call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields 
an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}

By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we 
can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- 
\autoref{fig:anonymous_onymous} contains a comprehensible summary.

\begin{figure}[t]
\centering
\begin{tabular}{|l|c|c|}
\hline
 & \textbf{Anonymous} & \textbf{Onymous} \\
\hline
\textbf{Relations} & Witnessless & Hermida-Jacobs \\
\hline
\textbf{Spans} & Vanilla & Aczel-Mendler \\
\hline
\end{tabular}
\caption{Comparison of anonymous and onymous settings for relations and spans.}
\label{fig:anonymous_onymous}
\end{figure}

%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ 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\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
%\end{definition}

%\begin{definition}[$F$-Relator]
%	For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion.
%\end{definition}
%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$.
%
%\begin{prop}
%	Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, 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}
\begin{definition}[Aczel-Mendler Bisimulation]
\todo{Explain in terms of span morphisms}. 


	A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram:
	\begin{equation*}\label{eq:acz-mend-diag}
		\begin{tikzcd}[ampersand replacement=\&]
			{X} \& R \& {Y} \\
			{FX} \& FR \& {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["\gamma", from=1-2, to=2-2]
			\arrow["{\beta}", 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{definition}
Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$
instead of $\Set$. It is worth noting that with this definition, if $R$ is a
relation, it does not necassirily mean that $FR$ is a relation as well.
%
\begin{definition}[Witnessless Bisimulation]
	A relation $R\subseteq X\times Y$ is a \emph{witnessless bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)^\dagger}\beta(y)$.
%	\begin{equation*}
%		\begin{tikzcd}[ampersand replacement=\&]
%			{X} \& R \& {Y} \\
%			{FX} \& \rel(F)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["{\beta}", from=1-3, to=2-3]
%			\arrow["{q_1}", from=2-2, to=2-1]
%			\arrow["{q_2}"', from=2-2, to=2-3]
%		\end{tikzcd}
%	\end{equation*}
\end{definition}
A more general version of witnessless bisimulation is given by Hughes and Jacobs, where the lifting is an arbitrary lifting not necessarily the one with image factorization that we mentioned here.

\begin{definition}[Hermida-Jacobs Bisimulation]
	A relation $R\subseteq X\times Y$ is a \emph{Hermida-Jacobs bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to (FR)^\dagger$ called witness that commutes in the following diagram:
	\begin{equation*}
		\begin{tikzcd}[ampersand replacement=\&]
			{X} \& R \& {Y} \\
			{FX} \& (FR)^\dagger \& {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["\gamma", from=1-2, to=2-2]
			\arrow["{\beta}", 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{definition}
Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.

\begin{definition}[Vanilla Bisimulation]\label{def:vanila}
	A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$.
%	\begin{equation*}
%		\begin{tikzcd}[ampersand replacement=\&]
%			{X} \& R \& {Y} \\
%			{FX} \& FR \& {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["{\beta}", 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{definition}
We do not know if this definition exists anywhere.
\begin{prop}
	The following propositions hold in $\Set$:
	\todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? }
	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
		%\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
		\item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
		\item Every Aczel-Mendler bisimulation is a Hermida-Jacobs bisimulation.
		\item Assuming the axiom of choice, every Hermida-Jacobs bisimulation is an Aczel-Mendler bisimulation.
		\item Every witnessless bisimulation is a Hermida-Jacobs bisimulation.
		%\item Every Hermida-Jacobs bisimulation is a witnessless bisimulation. 
	\end{enumerate}
\end{prop}
\begin{proof}
	%(I): ???%Assuming $x\mathrel{R}y$, then given by~\eqref{eq:acz-mend-diag} we have $\gamma(x,y)\in FR$, $Fp_1\comp\gamma(x,y)=\alpha(x)$, and $Fp_2\comp\gamma(x,y)=\beta(y)$ that means $\alpha(x)\mathrel{(FR)}\beta(y)$.
	
	(I): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}.
	
	(II):\autoref{lem:norm-simp}, and given by Staton.
	
	(III): Given by Staton, and similar to \autoref{lem:norm-simp}.
	
	(IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation.  
\end{proof}
\begin{rem}\todo{No, these definitions are just equivalent.}
	For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors.
\end{rem}
\begin{rem}
\todo{No, this does not follow from anythying.}   
	To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor.
\end{rem}
\todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}

\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}

%
\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}
%

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}
\todo{Prove that simulation in this sense of this definition is a standard simulation for powerset.}
\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.
\todo{So, $\sigma_3$ is a unique witness of bisimulation. How can we characterize it among all witnesses of simulation.}
%\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{prop: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{prop: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{prop: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}
\subsection{The concrete proof}
%\begin{lemma}\label{lem:sim-opsim-inc1}\ppnote{Actually, this lemma holds for every functor in an arbitrary category.}
%	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
%	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
%		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I1}
%		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II1}
%	\end{enumerate}
%\end{lemma}
%\begin{proof}
%	 By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
%	\begin{align}
%		\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_11}\\
%		\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_21}
%	\end{align}
%	(I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_21} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$. 
%	Therefore:
%	\begin{align*}
%	\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
%	=&\; \powf p_2\comp\sigma (x_2,x_1)\\
%	\subseteq&\;\alpha(x_1)\\
%	\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_11}}
%	\end{align*}
%	%
%	(II): Analogously, from~\eqref{eq:alpha_x_11} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
%	Therefore:
%	\begin{align*}
%	\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_21}}\\
%	\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
%	=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
%	=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& 
%	\end{align*}
%	\qed
%\end{proof}
\begin{lemma}\label{lem:sim-opsim-inc}
	In a category $\BC$, assuming that $F$ has a natural order structure $\appr$, and $\sigma\c R\to F R$ is witness for a symmetric relation $R$ to be an AM-simulation on $F$-coalgebra $(X,\alpha)$, then we have:
	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
		\item $F p_1\comp F s\comp\sigma\comp s\appr F p_1\comp\sigma$\label{item:sim-opsim-inc:I}
		\item $F p_2\comp\sigma\appr F p_2\comp F s\comp\sigma\comp s$\label{item:sim-opsim-inc:II}
	\end{enumerate}
\end{lemma}
\begin{proof}
	By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
	\begin{align}
		\alpha\comp p_1\appr&\;F p_1\comp\sigma,\label{eq:alpha_x_1}\\
		F p_2\comp\sigma\appr&\;\alpha\comp p_2.\label{eq:alpha_x_2}
	\end{align}
	(I): Since $R$ is symmetric and $\appr$ is a natural order structure, from \eqref{eq:alpha_x_2} we get $F p_2\comp\sigma\comp s\appr\alpha\comp p_2\comp s$. 
	Therefore:
	\begin{align*}
		F p_1\comp F s\comp\sigma\comp s=&\; F p_2\comp\sigma\comp s\\
		\appr&\;\alpha\comp p_2\comp s\\
		=&\;\alpha\comp p_1\\
		\appr&\; F p_1\comp\sigma & \by{\eqref{eq:alpha_x_1}}
	\end{align*}
	%
	(II): Analogously, from~\eqref{eq:alpha_x_1} since $R$ is symmetric and $\appr$ is a natural order structure, we get $\alpha\comp p_1\comp s\appr F p_1\comp\sigma\comp s$.
	Therefore:
	\begin{align*}
		F p_2\comp\sigma\appr&\; \alpha\comp p_2 &\by{\eqref{eq:alpha_x_2}}\\
		=&\; \alpha\comp p_1\comp s\\
		\appr&\; F p_1\comp\sigma\comp s \\
		=&\;F p_2\comp F s\comp\sigma\comp s.& 
	\end{align*}
	\qed
\end{proof}
We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
\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).
\end{gather*}
%\begin{lemma}
%	Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\join\sigma_2$ is also a witness that $R$ is an Aczel-Mendler simulation.
%\end{lemma}
%\begin{proof}
%	\todo{Finish.}
%\end{proof}
\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(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_1R_1$ or $x_1\in\powf p_1R_2$, respectively. So, we have $x_1\in \powf p_1R_1\cup\powf p_1R_2$.
	
	Now, assuming that $x_1\in\powf p_1R_1\cup\powf p_1R_2$ either $x_1\in\powf p_1R_1$ or $x_1\in\powf p_1R_2$. Without loss of generality, we can assume $x_1\in\powf p_1R_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(R_1\cup R_2)$.\qed
	%	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{rem}
%	Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
%\end{rem}
Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. 
\begin{prop}\label{prop:alph-prod}
	Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$. 
\end{prop}
\begin{proof}
	We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$.
	Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. 
	\qed
\end{proof}
An abstract version of the above proposition is given by Dubut that is the following:
\begin{prop}\label{prop:alph-prod-dubut}
	Assuming that $R$ is a relation, and $\sigma\c R\to FR$ is a witness for $R$ to be an AM-simulation, then there exists $\sigma'\c R\to FR$ that is another witness for $R$ to be an AM-simulation, such that $Fp_1\comp\sigma'=\alpha\comp p_1$. 
\end{prop}\qed
Now, we prove our main statement.
\begin{prop}\label{prop:sym-rel-bisim}
	Assuming that $R$ is a symmetric relation, and $\sigma\c R\to \powf R$ is a witness for $R$ to be a simulation, for which $\powf p_1\comp\sigma=\alpha\comp p_1$, then the following morphism is a witness for $R$ to be a bisimulation:
	\begin{gather*}
		\sigma\join(\powf s\comp\sigma\comp s)
	\end{gather*}
\end{prop}
\begin{proof}
	For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have 
	\begin{gather*}
		\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
		\powf p_1\comp\sigma(x_1,x_2).
	\end{gather*}
%	and by~\autoref{prop:alph-prod}, 
	Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
	\begin{gather*}
		\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
		\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).
	\end{gather*}
	Since $\powf p_1\comp\sigma=\alpha\comp p_1$ by precomposing $s$ to the both sides of the equation we get $\powf p_2\comp(\powf s\comp\sigma\comp s)=\alpha\comp p_2$. So, $\sigma\join(\powf s\comp\sigma\comp s)$ is a witness for $R$ to be an AM bisimulation.\qed
\end{proof}
\begin{cor}
	Considering~\autoref{prop:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well.
\end{cor}
Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
\subsection{Maybe Functor}
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$.\\
Now, we prove that the given order on the maybe functor is a liftable one.
\begin{lemma}\label{lem:maybe-lif}
	The order structure on the set-functor $FX=X+1$ is a liftable order.
\end{lemma}
\begin{proof}
	By~\autoref{lem:set-ord-str}, assuming $h\in\Hom(1,Y+1)$, $k\in\Hom(1,X+1)$, $g\c X\to Y$, and $h\appr (g+1)(k)$, we need to prove that exists $k'\in\Hom(1,X+1)$ such that $k'\appr k$ and $(g+1)(k')=h$. Since $h\in\Hom(1,Y+1)$ we have two cases:
	\begin{itemize}
		\item $h=\bot$: In this case we take $k'=\bot$, so we have $k'\appr k$, and then we have $g+1(k')=\bot=h$.  
		
		\item $g+1(k)=h$: In this case we take $k'=k$, then we have $g+1(k')=h$, and they are both an element of $Y$.\qed
	\end{itemize}
\end{proof}
So, proven by Dubut, for every symmetric AM-simulation relation over a coalgebra $(X,\alpha)$ of the maybe functor, we have a witness $\sigma\c R\to R+1$ such that $\alpha\comp p_1=(p_1+1)\comp\sigma$.
\begin{lemma}\label{lem:maybe-func-set}
	Assuming that $R$ is a symmetric AM-simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ either
	\begin{gather*}
		\alpha(x_1),\alpha(x_2)\in X,
	\end{gather*} 
	or
	\begin{gather*}
		\alpha(x_1)=\alpha(x_2)=\bot.
	\end{gather*}
\end{lemma}
\begin{proof}
	By~\autoref{prop:alph-prod-dubut} and~\autoref{lem:maybe-lif} there exists $\sigma\c R\to R+1$ that is a witness for $R$ to be an AM-simulation, and $p_1+1\comp\sigma=\alpha\comp p_1$. Since $R$ is symmetric, for every $(x_1,x_2)\in $ we have the following:
	\begin{enumerate}
		\item $\alpha(x_1)=p_1+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-1}
		\item $\alpha(x_2)=p_1+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-2}
		\item $\alpha(x_1)\sappr p_2+1\comp\sigma(x_2,x_1)$\label{eq:maybe-func-set-3}
		\item $\alpha(x_2)\sappr p_2+1\comp\sigma(x_1,x_2)$\label{eq:maybe-func-set-4}
	\end{enumerate}
	Now, we have two cases:
	\begin{itemize}
		\item Assuming $\alpha(x_1)\in X$ then by~\eqref{eq:maybe-func-set-1} we have $p_1+1\comp\sigma(x_1,x_2)\in X$, thus $\sigma(x_1,x_2)\in R$. So, we have $p_2+1\comp\sigma(x_1,x_2)\in X$ that by~\eqref{eq:maybe-func-set-4} means $\alpha(x_2)\in X$.
		\item Assuming $\alpha(x_1)=\bot$ then by~\eqref{eq:maybe-func-set-3} we have $p_2+1\comp\sigma(x_2,x_1)=\bot$, thus $\sigma(x_2,x_1)=\bot$. So, we have $p_1+1\comp\sigma(x_2,x_1)=\bot$ that by~\eqref{eq:maybe-func-set-2} means $\alpha(x_2)=\bot$ as well.\qed
	\end{itemize}
\end{proof}
%\begin{proof}
%	We assume that $\sigma\c R\to R+1$ is the witness that we have for $R$ to be an AM-simulation. We prove the statement by contradiction. If the statement is false, then we either have 
%	\begin{gather*}
%		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)=\bot,
%	\end{gather*}
%	or
%	\begin{gather*}
%		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)\in X.
%	\end{gather*}
%	Assuming $\alpha(x_1)\in X\;\&\; \alpha(x_2)=\bot$, then since $R$ is an AM-simulation, by~\eqref{eq:diag-lax-sim}$(p_2+1)\comp \sigma(x_1,x_2)\appr\alpha(x_2)$, we have $(p_2+1)\comp \sigma(x_1,x_2)=\bot$ that entails $\sigma(x_1,x_2)=\bot$. So, we have $(p_1+1)\comp \sigma(x_1,x_2)=\bot$, while $\alpha(x_1)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark
%	
%	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)\in X$, since $R$ is symmetric, then we have $(x_2,x_1)\in R$ as well. So, by~\eqref{eq:diag-lax-sim} we have $(p_2+1)\comp \sigma(x_2,x_1)\appr\alpha(x_1)$ that entails $\sigma(x_2,x_1)=\bot$. So, we have $(p_1+1)\comp\sigma(x_2,x_1)=\bot$, while  $\alpha(x_2)\not\sqsubseteq\bot$ that means that $\sigma$ is not a witness for $R$ to be an AM-simulation.\textreferencemark\qed
%\end{proof}

\begin{prop}\label{prop:sym-sim-bis-maybe}
	For a $F$-coalgebra $(X,\alpha)$ in $\Set$, such that $FX=X+1$, a symmetric AM-simulation relation $R$ on $X$ is an AM-bisimulation.
\end{prop}
\begin{proof}
	By~\autoref{lem:maybe-func-set} for every $(x_1,x_2)\in R$, we either have 
	\begin{gather*}
		\alpha(x_1)=\bot\quad\&\quad \alpha(x_2)=\bot,
	\end{gather*}
	or
	\begin{gather*}
		\alpha(x_1)\in X\quad\&\quad \alpha(x_2)\in X.
	\end{gather*}
	We define $\beta$ as a witness for $R$ to be an AM-bisimulation as follows:
	\begin{gather*}
		\beta(x_1,x_2)=
		\begin{cases} 
			\bot & \alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot  \\
			(\alpha(x_1),\alpha(x_2)) & \alpha(x_1)\in X\;\&\;\alpha(x_2)\in X
		\end{cases}
	\end{gather*}
	Assuming $\alpha(x_1)=\bot\;\&\; \alpha(x_2)=\bot$ we have $(p_i+1)\comp\beta(x_1,x_2)=\bot=\alpha(x_i)$, and assuming $\alpha(x_1)\in X\;\&\;\alpha(x_2)\in X$ we have $(p_i+1)\comp\beta(x_1,x_2)=\alpha(x_i)\in X$.
	Now, we are left to prove that if $\alpha(x_1)\in X$ and $\alpha(x_2)\in X$ then $\beta(x_1,x_2)\in R$ that means that the codomain of $\beta$ is indeed $R+1$. We assume $\alpha(x_i)\in X$. Since $\alpha(x_i)\in X=(p_i+1)\comp\beta(x_1,x_2)$ we have $\beta(x_1,x_2)\in R$. 
	\qed
\end{proof}

Now, we want to abstract the given proof for an extensive category that has terminal objects (so that we have the maybe functor). We assume a natural order structure $\appr$ for the maybe functor. For every objects $X$ and $Y$, we define $\appr$ on each $\Hom(X,Y+1)$ by saying that for $f,g\in\Hom(X,Y+1)$ we have $f\appr g$ whenever either $f=g$ or $f=\bot$.
%Although even in the context that we are at the moment, it does not seem plausible to prove that a symmetric simulation is a bisimulation without having an operator like $\join$ in~\autoref{prop:sym-sim-bis-maybe} that takes two morphisms of the same type and gives one.
\begin{lemma}\label{lem:maybe-lif-abs}
	The order structure on the functor $F\c\BC\to\BC$ defined as $FX=X+1$ is a liftable order.
\end{lemma}
\begin{proof}
	For morphisms $h\c X\to Z+1$, $g\c Y\to Z$, and $k\c X\to Y+1$, we assume $h\appr g+1\comp k$ that means we have two cases:
	\begin{itemize}
		\item $h=\bot$: In this case we take $k'=\bot$. Now, $k'\appr k$ and $g+1\comp k'=h$.
		\item $h=Fg\comp k$: In this case we take $k'=k$. Now, $k'\appr k$ and $g+1\comp k'=h$.\qed
	\end{itemize}
\end{proof}
To have an abstraction of~\autoref{lem:maybe-func-set} recalling that our category is extensive, we use the fact that for an arbitrary morphism $f\c X\to Y+Z$, we can have morphisms $f_Y\c X_Y\to Y$ and $f_Z\c X_Z\to Z$, such that $X_Y+X_Z\iso X$, so we follow with $f_Y+f_Z$. In our case, we take $\brks{\alpha\comp p_1,\alpha\comp p_2}\c R\to (X+1)\times(X+1)$, where $(X+1)\times (X+1)\iso X^2+(2\times X)+1$, and we assume the following pullbacks exist:
\begin{equation*}
	\begin{tikzcd}[ampersand replacement=\&]
		{R_{X^2}} \& R \& {R_{2\times X}} \& R \\
		{X^2} \& {X^2+(2\times X)+1} \& {(2\times X)} \& {X^2+(2\times X)+1} \\
		\& {R_1} \& R \\
		\& 1 \& {X^2+(2\times X)+1}
		\arrow["{q_1}", from=1-1, to=1-2]
		\arrow["{q_2}"', from=1-1, to=2-1]
		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-2, to=2-2]
		\arrow["{r_1}", from=1-3, to=1-4]
		\arrow["{r_2}"', from=1-3, to=2-3]
		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=1-4, to=2-4]
		\arrow["{\mathsf{in}_1}"', from=2-1, to=2-2]
		\arrow["{\mathsf{in}_2}"', from=2-3, to=2-4]
		\arrow["{s_1}", from=3-2, to=3-3]
		\arrow["{s_2}"', from=3-2, to=4-2]
		\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-2, to=4-3]
		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}", from=3-3, to=4-3]
		\arrow["{\mathsf{in}_3}"', from=4-2, to=4-3]
	\end{tikzcd}
\end{equation*}
%\begin{equation*}
%	\begin{tikzcd}[ampersand replacement=\&]
%		R \& I \& {X^2+(2\times X)+1}
%		\arrow["e", two heads, from=1-1, to=1-2]
%		\arrow["{\brks{\alpha\comp p_1,\alpha\comp p_2}}"', bend right=20, from=1-1, to=1-3]
%		\arrow["m", tail, from=1-2, to=1-3]
%	\end{tikzcd}
%\end{equation*}
So, we have the following:
\begin{gather*}
	R\iso R_{X^2}+R_{2\times X}+R_{1}
\end{gather*}
And now we can use $q_2+r_2+s_2\c R_{X^2}+R_{2\times X}+R_{1}\to X^2+(2\times X)+1$ instead of $\brks{\alpha\comp p_1,\alpha\comp p_2}$. To prove~\autoref{lem:maybe-func-set} abstractly is to prove that $q_2+r_2+s_2$ factors through $X^2+1$. To achieve this, we need to show that $R_{2\times X}\iso 0$. 
\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{definition}[Liftable Order Structure]\label{def:liftable-ord}
	A \emph{liftable 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}[Coliftable Order Structure]\label{def:coliftable-ord}
	A \emph{coliftable 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)$, and $g$ is surjective, 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:set-ord-str}
	In $\Set$, assuming that for every set $Y$ we have an order $\leq$ on $\Hom(1,FY)$ that satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, and if for $A\in\Hom(1,FZ)$, $B\in\Hom(1,FY)$, and $g\c Y\to Z$, $h\leq Fg(B)$ in $\Hom(1,FZ)$ there exists $B'\in\Hom(1,FY)$ such that $B'\leq B$ and $B\in\Hom(1,FY)$ and $A=Fg(B')$, then there exists an order structure $\appr$ on $F$ that is a liftable order structure. 
\end{lemma}
\begin{proof}
	For every $f,g\in\Hom(X,FY)$, we define $f\appr g$ whenever for all $x\in X$, $f(x)\leq g(x)$.
	
	Now, assuming $f\c X'\to X$, $\alpha,\beta\c X\to FY$, and $\alpha\appr\beta$, then for every $x'\in X'$, we have $\alpha(f(x'))\leq\beta(f(x'))$, so we have $\alpha\comp f\appr \beta\comp f$. Additionally, if we assume $g\c Y\to Y'$, then since $\leq$ satisfies \autoref{def:nat-ord}.\eqref{item:nat-ord:II}, for every $x\in X$ we have $Fg\comp\alpha(x)\leq Fg\comp\beta(x)$.
	
	Furthermore, if we have $g\c Y\to Z$, $k\c X\to FY$, $h\c X\to FZ$, and $Fg\comp k\appr h$, then for every $x\in X$ we have $Fg\comp k(x)\leq h(x)$, thus by the assumption of the lemma, for every $x$, there exists a set that we call $k'(x)$, for which we have $Fg(k'(x))\leq h(x)$. So, we have a function $k'\c X\to FY$, such that for every $x$ we have $Fg\comp k'(x)\leq h(x)$ that means $Fg\comp k'\appr h$.
	\qed
\end{proof}
\begin{remark}\label{rem:set-ord-str-co}
	The exact same argument in~\autoref{lem:set-ord-str} is true for coliftable order structures.
\end{remark}
\begin{lemma}\label{lem:liftable}
	Assuming that a a functor $F$ has an order structure $\appr$ that is liftable, 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$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, 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:liftable-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:coliftable}
	Assuming that a a functor $F$ has an order structure $\appr$ that is coliftable, then for every surjective $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 coliftable, 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:coliftable-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 coliftable 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 coliftable 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 coliftable order structure by~\autoref{def:coliftable-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}\label{prop:all-rel-compa}
	For a span $(\pi_1\c A\to X,\pi_2\c A\to Y)$, assuming that a set-functor $F$ has an order structure $\appr$, the following propositions hold:
	\begin{enumerate}
		\item If $\appr$ is liftable, 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 coliftable, 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 liftable and coliftable, 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:liftable} and~\autoref{lem:coliftable}. 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 liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$.
	
	Assuming $z\in\powf g(k')$, then there exists $y'\in \{y\mid g(y)\in h\}$ that $z=g(y')$, so $z\in h$ and $\powf g(k')\subseteq h$.
	
	Assuming $z\in h$, since $h\subseteq \powf g(k)$, then $z\in\powf g(k)$. So, there exists $y'\in k$ such that $g(y')=z$. So, by the definition of $k'$ we have $y'\in k'$ that means  $z\in\powf g(k')$.\qed
\end{example}
The following example justifies why the $g$ in~\autoref{def:coliftable-ord} should be surjective:
\begin{example}
	If we take the surjectivity of $g$ out of~\autoref{def:coliftable-ord}, subset relation over the powerset functor is NOT an example of a coliftable 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}
\begin{example}
	In the category of sets, subset over the powerset functor is an example of a coliftable order structure if the $g$ in~\autoref{def:coliftable-ord} is a surjective. Using~\autoref{rem:set-ord-str-co} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, $g\c Y\to Z$, such that $\powf g(k)\subseteq h$. We define $k'=k\cup\{y\mid g(y)\in h\}$, and we show that $\powf g(k')=h$.
	
	Obviously, $\powf g(k')\subseteq h$. Now, assuming $z\in h$ we prove that $z\in \powf g(k')$. Since $g$ is surjective, then exists $A\subseteq Y$ such that $\powf g(A)=h$. By the definition of $k'$, $A\subseteq k'$. So from $z\in h$ we have $z\in \powf g(A)$ that means that exists $a\in A$, such that $g(a)=z$. Now, since $A\subseteq k'$, then $a\in k'$. So, we have $z\in \powf g(k')$.\qed
\end{example}
\begin{definition}[Natural Relator]
	An $F$-relator $\relar$ is called \emph{natural}, whenever for every relation $r\c X\rto Y$, and all functions $f\c A\to X$, and $g\c B\to Y$, we have $\relar (g^\op\comp r\comp f)=(Fg)^\op\comp\relar r\comp Ff$.
\end{definition}
\begin{definition}[Relaional Connector]
	A natural $F$-relator $\relar$ is a \emph{relational connector}, whenever for every set $X$, $\id_{FX}\subseteq\relar\id_X$.
\end{definition}
\begin{definition}[Normal Relator]
	An $F$-relator $\relar$ is \emph{normal}, whenever for every set $X$, $\id_{FX}=\relar\id_X$.
\end{definition}
\begin{prop}
	Every normal relational connect is difunctionally functorial.\qed
\end{prop}

\begin{prop}
	Assuming that a set-functor $F$ has a liftable order structure $\appr$, then the $F$-relator $\relar r=\appr\comp Fr$ is natural. 
\end{prop}
\begin{proof}
	\begin{align*}
		\relar (g^\op\comp r\comp f)&\\
		=&\appr\comp F(g^\op\comp r\comp f)\\
		=&\appr\comp(Fg)^\op\comp Fr\comp Ff\\
		=&(Fg)^\op\comp\appr\comp Fr\comp Ff&\by{\autoref{lem:liftable}}\\
		=&(Fg)^\op\comp\relar r\comp Ff
	\end{align*}\qed
\end{proof}
\begin{remark}
	One may wonder if the above proposition is true for $F$-relators $r\mapsto Fr\comp\appr$ or $r\mapsto \appr\comp Fr\comp\appr$, where the order structure $\appr$ over $F$ is coliftable. But it may not be the case because the surjectivity condition on the $g$ in~\autoref{def:coliftable-ord} prevents the same reasoning.
\end{remark}
\begin{prop}
	Symmetrization of a natural relator, is natural.
\end{prop}
\begin{proof}
	Assuming $\relar$ is a natural $F$-relator, we prove that $\hat{\relar}$ is natural as well. Assuming $r\c X\rto Y$, $f\c A\to X$, and $g\c B\to Y$, by naturality of $\relar$ we have $\relar (g^\op\comp r\comp f)=Fg^\op\comp \relar r\comp Ff$. Then we have:
	\begin{align*}
		\hat{\relar}(g^\op\comp r\comp f)&\\
		=&\relar(g^\op\comp r\comp f)\cap(\relar(f^\op\comp r^\op\comp g))^\op\\
		=&(Fg)^\op\comp\relar r\comp Ff\cap((Ff)^\op\comp\relar r^\op\comp Fg)^\op\\
		=&(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff
	\end{align*}
	So we are left to prove
	\begin{gather*}
		(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff=(Fg)^\op\comp(\relar r\cap(\relar r^\op)^\op)\comp Ff
	\end{gather*}
	because then we will have $\hat{\relar}(g^\op\comp r\comp f)=(Fg)^\op\comp\hat{\relar}\comp Ff$. We have
	\begin{align*}
		(t,s)\in &(Fg)^\op\comp\relar r\comp Ff\cap (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
		&\iff(t,s)\in (Fg)^\op\comp\relar r\comp Ff\quad\&\quad (t,s)\in (Fg)^\op\comp(\relar r^\op)^\op\comp Ff,\\
		&\iff Ff(t) \mathrel{(\relar r)} Fg(s) \quad\&\quad Ff(t) \mathrel{(\relar r^\op)^\op} Fg(s),\\
		&\iff Ff(t) \mathrel{(\relar\cap(\relar r^\op)^\op)} Fg(s),\\
		&\iff t\mathrel{((Fg)^\op\comp(\relar\cap(\relar r^\op)^\op)\comp Ff)} s.
	\end{align*}
	It worth noting that when we have $(t,s)\in (Fg)^\op\comp\relar r\comp Ff$, it mean that there exist $t'$ and $s'$ that $(t,t')\in Ff$, $(t',s')\in \relar r$, and $(s',s)\in Fg^\op$. Since $Ff$ and $Fg$ are functions, then $t'=Ff(t)$ and $s'=Fg(s)$, and these are unique elements. The uniqueness enables us in the above reasoning to go from the second line to the third line.\qed 
\end{proof}
\begin{prop}
	If $\appr$ is an order structure on $F$ that for every sets $X$ and $Y$, $(\Hom(X,FY),\appr)$ is antisymmetric as well (making the posets), then the symmetrization of the left-lax Barr relator of $F$ and $\appr$ is normal.
\end{prop}
\begin{proof}
	We show the left-lax Barr relator with $\relar$. We have:
	\begin{align*}
		\hat{\relar}\id&\\
		=&\relar\id\cap(\relar\id^\op)^\op\\
		=&\appr\comp F\id\cap (\appr\comp F\id^\op)^\op\\
		=&\appr\cap\sappr\\
		=&\id
	\end{align*}\qed
\end{proof}
\begin{cor}
	Since the symmetrization of left-lax Barr relator that is laxed with a lifatble order structure is natural, and normal, it is a normal relational connector. So, it is a sound and complete relator.
\end{cor}
\begin{cor}
	By~\autoref{prop:all-rel-compa}.(1), if $\appr$ is liftable, then the mid-lax Barr relator is a normal relation connector, and thus a sound and complete relator as well.
\end{cor}
Perhaps if we can relax the definition of liftable by allowing $g$ to be a relation rather than a function, we can have a lax Barr relator that its symmetrization is a normal lax extension. Well, this idea actually does not work because if $g$ is supposed to be a relation, then $F$ can not be a set-functor, but it should be a functor on $\rel$, and it is already a big assumption.
\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 coliftable.
\end{prop}
\begin{proof}
	\todo{Investigate if it's true! If it is, is naturality necessary? It is really weird! If having a liftable 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 liftable 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}














