Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

draft/draft.tex

@@ -82,6 +82,8 @@
 \usetikzlibrary{arrows.meta}
 \usetikzlibrary{decorations}           % Required for all decorations
 \usetikzlibrary{decorations.pathmorphing} % Specifically for 'zigzag'
+\usetikzlibrary{matrix,positioning,arrows.meta,shapes.geometric}
+
 
 \tikzset{
   commutative diagrams/.cd,
@@ -104,6 +106,7 @@
 \usepackage{xspace}
 \usepackage{bm}
 \usepackage{pifont}
+\usepackage{circuitikz}
 
 \input{catprog}
 
@@ -308,7 +311,7 @@
 		}%
 	}%
 }
-\newcommand{\sub}{\mathcal{S}}
+\newcommand{\sub}{\mathcal{D}_{\leq1}}
 
 
 \newcommand{\bba}{
@@ -670,7 +673,7 @@ Now, we prove $Sg(\mu') = \nu$.
 %an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
 %We define the category of spans and relations.
 \begin{definition}[Category of Spans]\ppnote{Paul Levy said he doesn't like this name for this category as "category of spans" is used for a different category that is a bicategory.}
-	For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
+	For an arbitrary category $\BC$, the category of spans, denoted by $\spa(\BC)$ is the category that for every objects $R$, $X_1$ and $X_2$ in $\BC$, and every morphisms $p_1\c R\to X_1$, and $p_2\c R\to X_2$ in $\BC$, has an object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$, and for every morphisms $g_1\c X_1\to Y_1$, $g_2\c X_2\to Y_2$, and $w\c R\to S$ (called \emph{witness}) in $\BC$, has a morphism $(g_1,g_2,w)$ of type $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, whenever the following diagram commutes:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			{X_1} \& R \& {X_2} \\
@@ -685,11 +688,26 @@ Now, we prove $Sg(\mu') = \nu$.
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}
-
-\begin{definition}[Category of Relations]
-For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary -- it must have products. But this can be fixed by reformulating in terms of joint monics.}, the category of relations, denoted by $\rel(\BC)$ has as objects such spans $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ that $\brks{p_1,p_2}$ is a monomorphism. A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $(g_1,g_2,w)$ is a morphism in $\spa(\BC)$.
+%
+\begin{definition}[Jointly Monic]
+	A pair of morphisms $p_1\c R\to X$ and $p_2\c R\to Y$ 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:joint-mon-unique}
+	Given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$, assuming $q_1$ and $q_2$ are jointly monic, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then $w$ is unique.\qed
+\end{prop}
+%
+\begin{prop}\label{prop:joint-mon-pair}
+	In a category $\BC$ with products, two morphisms $p_1\c R\to X$ and $p_2\c R \to Y$ are jointly monic iff $\brks{p_1,p_2}\c R\to X\times Y$ is monic.\qed   
+\end{prop}
+%
+\begin{definition}[Category of Relations]
+For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is a full subcategory of $\spa(\BC)$ such that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel(\BC)$, $p_1$ and $p_2$ are jointly monic. %A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
+\end{definition}
+%\begin{remark}
+%	Followed by~\autoref{prop:joint-mon-unique}, given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel(\BC)$, for morphisms $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$ in $\BC$, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then for every $v\c R\to S$, such that $(g_1,g_2,v)$ is a morphism in $\rel(\BC)$, then $v=w$. 
+%\end{remark}
+%
 %\begin{prop}
 %	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel(\BC)$ and $\spa(\BC)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel(\BC)$.
 %\end{prop}
@@ -699,32 +717,62 @@ For an arbitrary category $\BC$\sgnote{In this definition $\BC$ is not arbitrary
 %
 \subsection{Spans and Relations in $\Set$}
 From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$ accordingly. There are two choices for defining morphisms in each of the categories $\spa$ and $\rel$, namely \emph{anonymous} and \emph{onymous}. The already introduced type of morphisms is onymous. For functions $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2) \to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ is an anonymous morphism in $\spa$ if:
-\begin{gather*}
+\begin{gather}\label{eq:ano-morph}
 	u\in R\Rightarrow \exists v\in S, q_1(v)= g_1\comp p_1(u) \quad\&\quad q_2(v)=g_2\comp p_2(u)
-\end{gather*}
-	In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that  forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
-\begin{gather*}
-	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
-\end{gather*}
+\end{gather}
+%	In case we are defining anonymous morphisms in $\rel$ we have the stronger version of the above property that  forces the elements of relations to be pairs and the existential quantifier refers to a unique element:
+%\begin{gather*}
+%	(x_1,x_2)\in R\Rightarrow (g_1(x_1),g_2(x_2))\in S
+%\end{gather*}
 From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and relations with anonymous morphisms, and $\spa$ and $\rel$ to denote the categories of spans and relations with onymous morphisms.
+\begin{lemma}\label{lem:rel-iso}
+	For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R'\subseteq X_1\times X_2$ and a bijection $r\c R\to R'$, such that
+	\begin{gather*}
+		\forall u\in R,\; p_1(u)=x_1\;\&\; p_2(u)=x_2\iff r(u)=(x_1,x_2).
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	By~\autoref{prop:joint-mon-pair} since $\Set$ has products $\brks{p_1,p_2}$ is monic. We take $R'$ as the image of $\brks{p_1,p_2}$ and we take $r\c R\to R'$ as the epimorphism in the image factorization of $\brks{p_1,p_2}$. Since $\brks{p_1,p_2}$ is monic, $r$ is a bijection. Now, the mentioned property is trivial.
+\end{proof}
+\begin{cor}\label{cor:rel-iso}
+	For every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel$, there exist $R'\subseteq X_1\times X_2$ and an bijection $r\c R\to R'$, such that for every $(x_1,x_2)\in R'$,
+	\begin{gather*}
+		p_1\comp r^{-1}(x_1,x_2)=x_1\quad\&\quad p_2\comp r^{-1}(x_1,x_2)=x_2.
+	\end{gather*}
+\end{cor}
+\begin{proof}
+	The mentioned $r$ exists by~\autoref{lem:rel-iso}. For every $(x_1,x_2)\in R'$ there exists a unique $u\in R$ such that $r(u)=(x_1,x_2)$, and it means that $p_1(u)=x_1$ and $p_2(u)=x_2$, so we have $u=r^\mone(x_1,x_2)$ that means $p_1\comp r^\mone(x_1,x_2)=x_1$ and $p_2\comp r^\mone(x_1,x_2)=x_2$.\qed
+\end{proof}
+%
 \begin{prop}\label{prop:rel-rela}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\rel_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the witness\sgnote{Unique?} $w\c R\to S$.
+Let $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$
+be jointly-monic spans. Then there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the unique witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
-	$(\Rightarrow):$ For every $(x_1,x_2)\in R$ we define $w$ as $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$. We have:
+%	$(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have:
+%	\begin{align*}
+%		g_1\comp p_1(x_1,x_2)&\\
+%		=&g_1(x_1)\\
+%		=&q_1(g_1(x_1),g_2(x_2))\\
+%		=&q_1\comp w(x_1,x_2)
+%	\end{align*}
+%	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
+	$(\Rightarrow)$: By~\autoref{lem:rel-iso} there exist bijections $r\c R\to R'$ and $s\c S\to S'$ with the mentioned property. Since $(g_1,g_2)$ is a morphism from $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ to $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, for every $(x_1,x_2)\in R'$ we have $(g_1(x_1),g_2(x_2))\in S'$. So, we define $w'\c R'\to S'$ as $w'(x_1,x_2)=(g_1(x_1),g_2(x_2))$, and we define $w\c R\to S$ as $w=s^\mone\comp w'\comp r$. For every $u\in R$ and $i\in\{1,2\}$ we have:
 	\begin{align*}
-		g_1\comp p_1(x_1,x_2)&\\
-		=&g_1(x_1)\\
-		=&q_1(g_1(x_1),g_2(x_2))\\
-		=&q_1\comp w(x_1,x_2)
+		q_i\comp w(u)\\
+		=&q_i\comp s^\mone\comp w'\comp r(u)\\
+		=&q_i\comp s^\mone\comp w'(x_1,x_2)\\
+		=&q_i\comp s^\mone(g_1(x_1),g_2(x_2))\\
+		=&g_i(x_i)&\by{\autoref{cor:rel-iso}}\\
+		=&g_i(p_i(u))\\
+		=&g_i\comp p_i(u)
 	\end{align*}
-	Similarly, we have $g_2\comp p_2(x_1,x_2)=q_2\comp w(x_1,x_2)$.
 	
-	$(\Leftarrow):$ Assuming $x_1\mathrel{R}x_2$, then $w(x_1,x_2)\in S$ as well, and by the definition of onymous morphisms we have $w(x_1,x_2)=(g_1(x_1),g_2(x_2))$, so we have $g_1(x_1)\mathrel{S}g_2(x_2)$. \qed
+	$(\Leftarrow):$ Assuming $u\in R$ we take $w(u)\in S$ as $v$ in~\eqref{eq:ano-morph}. We have $q_1(w(u))=p_1\comp g_1(u)$ and $q_2(w(u))=p_2\comp g_2(u)$ since $(g_1,g_2,w)$ is the morphism of the mentioned type.\qed
 \end{proof}
 
 \begin{prop}\label{prop:spa-spaa}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\spa$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\spa$, with the witness $w\c R\to S$.
 \end{prop}
 \begin{proof}
 	($\Rightarrow$): We need the axiom of choice to prove this statement. By the definition of anonymous morphisms, for every $u\in R$ there exists $v\in S$ such that $q_1(v)=p_1\comp g_1(u)$ and $q_2(v)=p_2\comp g_2(u)$. So, for each $u\in R$ there exists a set $V_u\in\powf S$ that its elements have the mentioned properties. We can form a function $h\c R\to \powf S$ that $h(u)=V_u$. The image of $h$ that we denote with $\im(h)$ is a family of non-empty sets. By the axiom of choice, there exists a function $s\c \im(h)\to S$. We define $w\c R\to S$ as $w=s\comp h$, then for every $u\in R$, we have $q_1\comp w(u)=g_1\comp p_1(u)$ and $q_2\comp w(u)=g_2\comp p_2(u)$.
@@ -732,38 +780,64 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 	($\Leftarrow$): Assuming $u\in R$, there exists $w(u)\in S$, and by the definition of onymous morphisms we have $q_1(w(u))=g_1\comp p_1(u)$ and $q_2(w(u))=g_2\comp p_2(u)$. \qed
 \end{proof}
 
-\begin{prop}\label{prop:rela-spaa}\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
+\begin{prop}\label{prop:rela-spaa}%\sgnote{This becomes trivial, if we define Rel as full subcategory of Span.}
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel_a$ and $\spa_a$, there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa_a$ iff there is a morhpism $(g_1,g_2)$ of the same type in $\rel_a$.
 \end{prop}
 \begin{proof}
-	($\Rightarrow$): Assuming that $(g_1,g_2)$ is a morphism in $\spa_a$, then for $(x_1,x_2)\in R$ there exists $v\in S$, such that $q_1(v)=g_1(x_1)$ and $q_2(v)=g_2(x_2)$. Since $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)\in\rel_a$ then the $v$ is unique and $v=(g_1(x_1),g_2(x_2))$. 
-	
-	($\Leftarrow$): As $\rel_a$ is a subcategory of $\spa_a$, this is trivial.\qed
+	It is trivial as $\rel_a$ is a full subcategory of $\spa_a$\qed
 \end{proof}
 
 \begin{prop}\label{prop:rel-spa}
-	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel$ and $\spa$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$.
+	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects of both categories $\rel$ and $\spa$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel$.
 \end{prop}
 \begin{proof}
 	Trivial by the definitions.\qed
 \end{proof}
+%\begin{figure}[t]
+%	\centering
+%	\begin{tabular}{|l|c|c|c|c|}
+%		\hline
+%		\quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\
+%		\hline
+%		$\spa$ &  & & & \\
+%		\hline
+%		$\rel$ & & & & \\
+%		\hline
+%		$\spa_a$ & \ding{56} & & & \\
+%		\hline
+%		$\rel_a$ & & & & \\
+%		\hline
+%	\end{tabular}
+%	\caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column is in $\Set$.}
+%	\label{fig:anonymous_onymous-choice}
+%\end{figure}
 \begin{figure}[t]
 	\centering
-	\begin{tabular}{|l|c|c|c|c|}
-		\hline
-		\quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\
-		\hline
-		$\spa$ &  & & & \\
-		\hline
-		$\rel$ & & & & \\
-		\hline
-		$\spa_a$ & \ding{56} & & & \\
-		\hline
-		$\rel_a$ & & & & \\
-		\hline
-	\end{tabular}
-	\caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column exists, in $\Set$.}
-	\label{fig:anonymous_onymous-choice}
+	\begin{tikzpicture}[
+		scale=0.6, every node/.style={transform shape}
+		]
+		\matrix (m) [matrix of nodes,
+		nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
+			align=center, font=\scriptsize, inner sep=2pt},
+		row sep=6mm, column sep=6mm]
+		{
+			$\spa$   & $\spa_a$ \\
+			$\rel$   & $\rel_a$   \\
+		};
+		
+		% Example arrows (uncomment / edit as needed):
+		\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10]  (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, above] {AC}  (m-1-1);
+		\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10]  (m-2-2);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10]  (m-2-1);
+		\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10]  (m-2-1);
+		\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10]  (m-1-1);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10]  (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10]  (m-2-2);
+%		
+	\end{tikzpicture}
+	\caption{Summary of results in this section about when we have a morphism in the source of an arrow then we have a morphism in the target in $\Set$.}
+	\label{fig:morph-summery}
 \end{figure}
 %\begin{notation}
 %	In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$.
@@ -1189,28 +1263,28 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta
 %\todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}\\
 %--------------------------------------------------------------
 \begin{definition}[Aczel-Mendler Bisimulation]
-	In an arbitrary category $\BC$, a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.   
+	Given an arbitrary category $\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa(\BC)$ is an \emph{Aczel-Mendler bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\spa(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$.   
 \end{definition}
 %
-\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$, whenever 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["{U}"',from=1-1, to=2-1]
-			\arrow["{U}",from=1-3, to=2-3]
-			\arrow["{F\times F}"', from=2-1, to=2-3]
-		\end{tikzcd}
-	\end{equation*}
-\end{definition}	
-\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis}
-	In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.   
-\end{definition}
-The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
+%\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$, whenever 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["{U}"',from=1-1, to=2-1]
+%			\arrow["{U}",from=1-3, to=2-3]
+%			\arrow["{F\times F}"', from=2-1, to=2-3]
+%		\end{tikzcd}
+%	\end{equation*}
+%\end{definition}	
+%\begin{definition}[Abstract Relational Bisimulation]\label{def:abs-rel-bis}
+%	In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an \emph{abstract relational bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$.   
+%\end{definition}
+%The given definition is highly abstract. There is a relation lifting that abstracts Barr-relators that are known to be well-behaved relators, and it also gives an interesting notion of bisimulation, called \emph{Hermida-Jacobs bisimulation}.
 %
-	The lifting is using 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.}
+%	The lifting is using 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=\&]
@@ -1220,35 +1294,69 @@ The given definition is highly abstract. There is a relation lifting that abstra
 		%		\arrow["{\brks{p^\dagger_1,p^\dagger_2}}"', tail, from=1-2, to=1-4]
 		%	\end{tikzcd}
 	%\end{equation*}
-	For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\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^\clubsuit} \&\& {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^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4]
-		\end{tikzcd}
-	\end{equation*}
-	Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
-	So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ 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*}
+	By applying the functor $F$ on all of the components of $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ that is an object of $\spa(\BC)$ we get another object of $\spa(\BC)$, but it is not the case for $\rel(\BC)$. As an example, if we set $F$ to be the powerset functor $\powf$, then $(\powf X \stackrel{\powf p_1}{\leftarrow} \powf R \stackrel{\powf p_2}{\to}\powf Y)$ is not necessarily a relation anymore because if we take $R=\{(1,0),(0,1),(0,0),(1,1)\}$, and define functions $f\c R\to \powf R$ and $g\c R\to \powf R$ as
+	\begin{gather*}
+		f(w)=
+		\begin{cases} 
+			\{(1,0),(0,1),(0,0),(1,1)\} & w=(0,0)  \\
+			R & otherwise
+		\end{cases}\\
+		g(w)=
+		\begin{cases} 
+			\{(1,0),(0,1),(0,0)\} & w=(0,0)  \\
+			R & otherwise
+		\end{cases}
+	\end{gather*}
+	 then $\powf p_1\comp f=\powf p_1\comp g$ and $\powf p_2\comp f=\powf p_2\comp g$ hold, but $f\neq g$. So, $\powf p_1$ and $\powf p_2$ are not jointly monic.
+%	For a regular category $\BC$, we define a functor of type $(-)^\clubsuit\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^\clubsuit} \&\& {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^\clubsuit_1,p^\clubsuit_2}}"', tail, from=1-2, to=1-4]
+%		\end{tikzcd}
+%	\end{equation*}
+%	Also, for every functor $F\c\BC\to\BC$ we have a trivial lifting to $\spa(\BC)$ that takes every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$, and every morphism $(f,g,w)$ to $(Ff,Fg,Fw)$, and we denote it with $\spa(F)$. Since $\rel(\BC)$ is a subcategory of $\spa(\BC)$, we have an inclusion functor $I\c\rel(\BC)\to\spa(\BC)$ as well.
+%	So, given a functor $F\c\BC\to\BC$ we define its lifting $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ as $(F-)^\dagger=(\spa(F)I-)^\clubsuit$. The functor $(F-)^\dagger$ 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*}
+To cope with this, we assume $\BC$ to be a regular category, so we have the following epi-mono decomposition for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa(\BC)$:
+\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*}
+We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(X \stackrel{p^\dagger_1}{\leftarrow} R^\dagger \stackrel{p^\dagger_2}{\to}Y)$, then we define $(F-)^\dagger\c\rel(\BC)\to\rel(\BC)$ to take $(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ 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*}
 %
 \begin{definition}[Hermida-Jacobs Bisimulation]
-	In an arbitrary category $\BC$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, if there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.   
+	Given a regular category $\BC$, an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is a \emph{Hermida-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, whenever there exists a morphism in $\rel(\BC)$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.   
 \end{definition}
 %
 \begin{lemma}\label{lem:morph-spa-rel}
-	In a regular category $\BC$ with the axiom of choice, assuming that $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$ is an object in $\spa(\BC)$, if for an object $A$ in $\BC$ we have a morphism $w\c A\to S^\dagger$, then there exist a morphism $v\c A\to S$ such that for $i\in\{1,2\}$, we have $q_i\comp v=q_i^\dagger\comp w$.
+	In a regular category $\BC$ with the axiom of choice, assuming that $(Y_1 \stackrel{q^\dagger_1}{\leftarrow} S^\dagger \stackrel{q^\dagger_2}{\to}Y_2)$ is an object in $\spa(\BC)$, if for an object $A$ in $\BC$ we have a morphism $w\c A\to S^\dagger$, then there exists a morphism $v\c A\to S$ such that for $i\in\{1,2\}$, we have $q_i\comp v=q_i^\dagger\comp w$.
 \end{lemma}
 \begin{proof}
 	Having the axiom of choice in a regular category $\BC$ means that for $e_S\c S\to S^\dagger$ there exist a section $s$. We define $v=s\comp w$, then for $i\in\{1,2\}$ we have:
@@ -1277,14 +1385,34 @@ The given definition is highly abstract. There is a relation lifting that abstra
 %\end{proof}
 %
 \begin{prop}\label{prop:HeJ-AM}
+	Given a regular category $\BC$, we have the following:
 	\begin{enumerate}
-		\item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an AM-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is a HJ-bisimulation.
-		\item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-bisimulation on coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an AM-bisimulation.
+		\item If an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an AM-bisimulation on $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an HJ-bisimulation.
+		\item If every regular epimorphism in $\BC$ has a section, assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an HJ-bisimulation on $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$ then it is an AM-bisimulation.
 	\end{enumerate}
 \end{prop}
 \begin{proof}
-	$(1)$: Trivial.\\
-	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\qed
+	$(1)$: The proof is trivial if we define the witness $\sigma^\dagger\c R\to(FR)^\dagger$, such 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 commutative diagram:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			X \& R \& Y \\
+			FX \& FR \& FY \\
+			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["{{\sigma}}", from=1-2, to=2-2]
+			\arrow["\beta", 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*}
+	$(2)$:  Since $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-bisimulation we have a morhpism $(\alpha,\beta,\sigma^\dagger)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp^\dagger_1}{\leftarrow} (FR)^\dagger \stackrel{Fp^\dagger_2}{\to}FY)$ in $\rel(\BC)$. By~\autoref{lem:morph-spa-rel}, there exists $\sigma\c R\to FR$ such that $(\alpha,\beta,\sigma)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ is a morphism in $\rel(\BC)$.\qed
 \end{proof}
 %
 \subsection{Coalgebraic Bisimulation in Set}
@@ -1301,9 +1429,9 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 \begin{prop}
 	In $\Set$, for $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, 
 	\begin{enumerate}
-		\item Assuming the axiom of choice span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation.
-		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation.
-		\item A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.
+		\item Assuming the axiom of choice an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\spa$ is an Aczel-Mendler bisimulation iff it is a span-based bisimulation.
+		\item An object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ is a Hermida-Jacobs bisimulation iff it is a Hughes-Jacobs bisimulation.
+		\item An object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ is a span-based bisimulation iff it is a Hughes-Jacobs bisimulation.
 	\end{enumerate}
 \end{prop}
 \begin{proof}
@@ -1311,8 +1439,8 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 	
 	(2): Follows from~\autoref{prop:rel-rela}.
 	
-	(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $(x,y)\in R$ there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\
-	($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $(x,y)\in R$ there then $(\alpha(x),\beta(y))\in(FR)^\dagger$ that means that exists $u\in FR$ such that $Fp_1(u)=\alpha(x)$ and $Fp_2(u)=\beta(u)$, and it exactly means that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation.
+	(3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then by the assumption there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\
+	($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then there exists $v^\dagger\in(FR)^\dagger$ such that $(Fp_1)^\dagger(v^\dagger)=\alpha(x)$ and $(Fp_2)^\dagger(v^\dagger)=\beta(y)$, and since $(FR)^\dagger$ by definition is the image of $\brks{Fp_1,Fp_2}$, so $(FR)^\dagger\subseteq FX\times FY$ that entails $v^\dagger=(\alpha(x),\beta(y))$. Furthemore, since $(\alpha(x),\beta(y))\in(FR)^\dagger$, there exists $v\in FR$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, so we have the morphism that we want, to be able to say that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation.
 	\qed
 \end{proof}
 \begin{cor}
@@ -1335,22 +1463,50 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 %
 \begin{figure}[t]
 	\centering
-	\begin{tabular}{|l|c|c|c|c|}
-		\hline
-		\qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\
-		\hline
-		Aczel-Mendler &  & & & \\
-		\hline
-		Hermida-Jacobs & \ding{56} & & & \\
-		\hline
-		Span-based & \ding{56} & & & \\
-		\hline
-		Hughes-Jacobs & \ding{56} & & & \\
-		\hline
-	\end{tabular}
-	\caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.}
-	\label{fig:bisim-choice}
+	\begin{tikzpicture}[
+		scale=0.6, every node/.style={transform shape}
+		]
+		\matrix (m) [matrix of nodes,
+		nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
+			align=center, font=\scriptsize, inner sep=2pt},
+		row sep=6mm, column sep=6mm]
+		{
+			Hughes-Jacobs   & Hermida-Jacobs \\
+			Span-based   & Aczel-Mendler   \\
+		};
+		
+		% Example arrows (uncomment / edit as needed):
+		\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10]  (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10]  (m-1-1);
+		\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] node[midway, below] {AC}   (m-2-2);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10]  (m-2-1);
+		\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10]  (m-2-1);
+		\draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10]  (m-1-1);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10]  (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, left] {AC}  (m-2-2);
+		%		
+	\end{tikzpicture}
+	\caption{Summery of results in this section about notions of bisimulation in $\Set$.}
+	\label{fig:bisim-summery}
 \end{figure}
+%\begin{figure}[t]
+%	\centering
+%	\begin{tabular}{|l|c|c|c|c|}
+%		\hline
+%		\qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\
+%		\hline
+%		Aczel-Mendler &  & & & \\
+%		\hline
+%		Hermida-Jacobs & \ding{56} & & & \\
+%		\hline
+%		Span-based & \ding{56} & & & \\
+%		\hline
+%		Hughes-Jacobs & \ding{56} & & & \\
+%		\hline
+%	\end{tabular}
+%	\caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.}
+%	\label{fig:bisim-choice}
+%\end{figure}
 \section{Coalgebraic Simulation}
 %\todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.}
 \begin{definition}[Aczel-Mendler Simulation]
@@ -1374,7 +1530,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 %
 \begin{definition}[Hermida-Jacobs Simulation]
 	Assuming that $\appr$ is a natural order structure on a functor $F\c\BC\to\BC$, an $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\rel(\BC)$ is a \emph{Hermida-Jacobs simulation} from a coalgebra $(X,\alpha)$ to $(Y,\beta)$, whenever the following diagram commutes laxly:
-	\begin{equation*}\label{eq:diag-hj-sim}
+	\begin{equation}\label{eq:diag-hj-sim}
 		\begin{tikzcd}[ampersand replacement=\&]
 			X \& R \& Y \\
 			FX \& (FR)^\dagger \& FY
@@ -1388,21 +1544,139 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 			\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{equation}
 \end{definition}
 %
 \begin{prop}
+	In a regular category $\BC$ the following propositions hold:
 	\begin{enumerate}
-		\item Assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$\sgnote{Is it a relation or a general span?} is an AM-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is a HJ-simulation.
-		\item In a regular category $\BC$ with the axiom of choice, assuming $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a HJ-simulation from a coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an AM-simulation.
+		\item Assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an AM-simulation from an $F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an HJ-simulation.
+		\item In a regular category $\BC$ with the axiom of choice, assuming an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-simulation from an $F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ then it is an AM-simulation.
 	\end{enumerate}
 \end{prop}
 \begin{proof}
-	$(1)$: Trivial.\sgnote{Does not look so trivial.}\\
-	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\sgnote{Add more details.}\qed
+	$(1)$: 
+	We have the following lax commutative diagram:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			X \& R \& Y \\
+			FX \& FR \& FY \\
+			FX \& {(FR)^\dagger} \& FY
+			\arrow["\alpha"', from=1-1, to=2-1]
+			\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=1-1, to=2-2]
+			\arrow["{{p_1}}"', from=1-2, to=1-1]
+			\arrow["{{p_2}}", from=1-2, to=1-3]
+			\arrow["{{\sigma}}", from=1-2, to=2-2]
+			\arrow["\beta", from=1-3, to=2-3]
+			\arrow["\id"', from=2-1, to=3-1]
+			\arrow["\sqsubseteq"{marking, allow upside down}, draw=none, from=2-2, to=1-3]
+			\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*}
+	We define $\sigma^\dagger\c R\to(FR)^\dagger$ such that $\sigma^\dagger=e_{FR}$. Then we have 
+	\begin{align*}
+		\alpha\comp p_1&\\
+		&\appr Fp_1\comp\sigma\\
+		&=(Fp_1)^\dagger\comp e_{FR}\comp\sigma\\
+		&=(Fp_1)^\dagger\comp \sigma^\dagger,
+	\end{align*}
+	and
+	\begin{align*}
+		Fp_2\comp\sigma&\\
+		&=(Fp_2)^\dagger\comp e_{FR}\comp\sigma\\
+		&=(Fp_2)^\dagger\comp\sigma^\dagger\\
+		&\appr\beta\comp p_2
+	\end{align*}
+	$(2)$: Since $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ is an HJ-simulation we have a morhpism $\sigma^\dagger\c R\to(FR)^\dagger$ that laxly commutes in~\eqref{eq:diag-hj-sim}. By~\autoref{lem:morph-spa-rel}, there exists $\sigma\c R\to FR$ that laxly commutes in~\eqref{eq:diag-am-sim}.\qed
 \end{proof}
 %
 \subsection{Simulations in Set}
+
+%\begin{figure}[ht]
+%	\centering
+%	\begin{tabular}{|c|c|c|c|c|}
+%		\hline
+%		 & \textbf{Hughes-Jacobs} & \textbf{Hermida-Jacobs} & \textbf{Span-based} & \textbf{Aczel-Mendler} \\
+%		\hline
+%		$\appr\cdot-$ & ? & ? & ? & ? \\
+%		\hline
+%		$-\cdot\appr$ & ? & ? & ? & ? \\
+%		\hline
+%		$\appr\cdot-\cdot\appr$ & ? & ? & ? & ? \\
+%		\hline
+%	\end{tabular}
+%	\caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.}
+%	\label{fig:anonymous_onymous_transposed}
+%\end{figure}
+\begin{figure}[t]
+	\centering
+	\begin{tikzpicture}[
+		scale=0.6, every node/.style={transform shape}
+		]
+		\matrix (m) [matrix of nodes,
+		nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
+			align=center, font=\scriptsize, inner sep=2pt},
+		row sep=6mm, column sep=6mm]
+		{
+			AM-simulation   & left-lax simulation\\
+			& bi-lax simulation   & mid-lax simulation   \\
+			HJ-simulation & left-lax simulation\\
+		};
+		
+		% Example arrows (uncomment / edit as needed):
+		\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1);
+		\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3);
+		\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3);
+		\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30]  (m-3-2);
+		\draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2);
+		\draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2);
+		\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1);
+		\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
+		
+	\end{tikzpicture}
+	\caption{Summary of results in this section about notions of simulation in $\Set$.}
+	\label{fig:sim-summery}
+\end{figure}
+%\begin{center}
+%\begin{tikzpicture}[
+%    scale=0.6, every node/.style={transform shape}
+%]
+%\matrix (m) [matrix of nodes,
+%             nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm,
+%                    align=center, font=\scriptsize, inner sep=2pt},
+%             row sep=6mm, column sep=6mm]
+%{
+%  AM-simulation   & left-lax simulation\\
+%  & bi-lax simulation   & mid-lax simulation   \\
+%  HJ-simulation & left-lax simulation\\
+%};
+%
+%% Example arrows (uncomment / edit as needed):
+%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1);
+%\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1);
+%\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3);
+%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2);
+%\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3);
+%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30]  (m-3-2);
+%\draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
+%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2);
+%\draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2);
+%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2);
+%\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1);
+%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
+%
+%\end{tikzpicture}
+%\end{center}
+
 Traditionally, simulations in $\Set$ are defined using relators. In this section we make a comparison on this concept with the other notions of simulation that we mentioned.
 %\begin{notation}
 %	We show the category of sets and binary relations with $\rels$, and we show a morphism in this category as $R\c X\rto Y$ that is a relation $R$.
@@ -1417,7 +1691,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 %\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]\label{def:relator}
-	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\Rel$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$. 
+	Assuming $F$ is a functor on $\Set$, an $F$-relator or simply a relator $\relar$ is a monotone map that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ of $\Rel$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$. 
 \end{definition}
 %
 %\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim-rela}
@@ -1450,28 +1724,81 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 \end{definition}
 %
 \begin{example}
-	Given $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation.
+	Given a functor $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation.
 \end{example}
 %
-\begin{example}
-	Given $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{q_2}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote this relator with $F^\leftrightarrow$.
+\begin{lemma}\label{lem:rel-rep}
+	Given a functor $F\c\Set\to\Set$, for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$, we have $(FR)^\dagger=Fp_2\comp (Fp_1)^\op$.
+\end{lemma}
+\begin{proof}
+	Since $(FR)^\dagger$ is the image of $\brks{p_1,p_2}$, we have $(FR)^\dagger\subseteq FX\times FY$. For every $x\in FX$ and $y\in FY$ we have $x\mathrel{(FR)^\dagger}y$ iff there exists a unique $u\in FR$ such that $\brks{Fp_1,Fp_2}(u)=(x,y)$, and the latter holds if and only if $(x,y)=(Fp_1(u),Fp_2(u))$, and it is equivalent with saying that $x\mathrel{(FR)^\dagger}y$.\qed 
+\end{proof}
+%
+\begin{example}\label{ex:lax-rels}
+	Given a functor $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{(Fp_2)^\dagger}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote a bi-lax Barr relator of a functor $F$ with $\tilde{F}$.\\
+	Additionally, followed by~\autoref{lem:rel-rep} we have \emph{mid-lax} relator. This relator sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} Fp_2\comp\appr\comp (Fp_1)^\op \stackrel{(Fp_2)^\dagger}{\to}FY)$.
 \end{example}
 %
-\begin{prop}\label{prop:HeJ-HuJ}
-	For a functor $F\c\Set\to\Set$, every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ from a coalgebra $(X,\alpha)$ to $(Y,\beta)$:
+\begin{prop}
+	For an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ that $p_1$ and $p_2$ are surjective, assuming that a set-functor $F$ has a natural order structure $\appr$, the following propositions hold:
 	\begin{enumerate}
-		\item is a $F^\leftrightarrow$-simulation  if it is a Hermida-Jacobs simulation.
-		\item is a Hermida-Jacobs simulation if it is a $F^\leftrightarrow$-simulation, assuming the axiom of choice.
+		\item If $\appr$ is liftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad Fp_2\comp(Fp_1)^\op\comp\appr$
+		\item If $\appr$ is coliftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad \appr\comp Fp_2\comp(Fp_1)^\op$
+		\item If $\appr$ is both liftable and coliftable, all the following are equal:
+		\begin{itemize}
+			\item $Fp_2\comp\appr\comp(Fp_1)^\op\quad$
+			\item $Fp_2\comp(Fp_1)^\op\comp\appr$
+			\item $\appr\comp Fp_2\comp(Fp_1)^\op$
+			\item $\appr\comp Fp_2\comp(Fp_1)^\op\comp\appr$
+		\end{itemize}
 	\end{enumerate}
 \end{prop}
 \begin{proof}
-	(1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $(x,y)\in R$, we have $\alpha\comp p_1(x,y)\appr(Fp_1)^\dagger\comp\sigma(x,y)$ and $(Fp_2)^\dagger\comp\sigma(x,y)\appr\beta\comp p_2(x,y)$. So, $x\mathrel{R}y$ gives that $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means that $R$ is a $F^\leftrightarrow$-simulation.\\
-	(2): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a $F^\leftrightarrow$-simulation means that $x\mathrel{R}y$ gives $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $(x,y)\in R$, there exist $(u,v)\in(FR)^\dagger$ such that $\alpha(x)\appr u$ and $v\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $(x,y)$ to the set of the mentioned existing pairs $(u,v)$ in $(FR)^\dagger$. By the axiom of choice there exist a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$.\qed
+	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{cor}
+	Assuming that the order structure $\appr$ on a functor $F\c\Set\to\Set$ is liftable and coliftable, all the notions of simulation given by relators mentioned in~\autoref{ex:lax-rels}
+	are equivalent.
+\end{cor}
+%
+\begin{prop}\label{prop:HeJ-HuJ}
+Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$,
+	\begin{enumerate}
+		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.
+		\item $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hermida-Jacobs simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a $\tilde{F}$-simulation, assuming the axiom of choice.
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	(1): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a Hermida-Jacobs simulation means that for every $u\in R$ that $p_1(u)=x$ and $p_2(u)=y$, we have $\alpha(x)\appr(Fp_1)^\dagger\comp\sigma(u)$ and $(Fp_2)^\dagger\comp\sigma(u)\appr\beta(y)$. Since $(FR)^\dagger\subseteq FX\times FY$, so $\sigma(u)$ is a pair $(v_1,v_2)\in(FR)^\dagger$ such that $\alpha(x)\appr v_1$ and $v_2\appr\beta(y)$, and it means that $\alpha(x)\appr\comp(FR)^\dagger\comp\appr\beta(y)$.
+	
+	(2): As $(\appr\comp(FR)^\dagger\comp\appr)\subseteq FX\times FY$, the object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ being an $\tilde{F}$-simulation means that for an arbitrary $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, we have $\alpha(x)\mathrel{(\appr\comp(FR)^\dagger\comp\appr)}\beta(y)$ that means for every $u\in R$, there exist $(v_1,v_2)\in(FR)^\dagger$ such that $\alpha(x)\appr v_1$ and $v_2\appr\beta(y)$. We form a function $f\c R\to\powf(FR)^\dagger$ such that takes every $u$ to the set of the mentioned existing pairs $(v_1,v_2)$ in $(FR)^\dagger$. By the axiom of choice there exists a function $s\c\im_f\to(FR)^\dagger$. So, assuming that $f$ has the epi-mono factorization $(e,m)$, then we define $\sigma\c R\to(FR)^\dagger$ as $\sigma=s\comp e$. Now, the diagram~\eqref{eq:diag-hj-sim} commutes laxly for the defined $\sigma$ as $(Fp_1)^\dagger\comp\sigma(u)=v_1$ and $(Fp_2)^\dagger\comp\sigma(u)=v_2$.\qed
 \end{proof}
 \begin{rem}
 	The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.
 \end{rem}
 Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it!
+%\begin{equation}
+%	\begin{figure}[!ht]
+%		\centering
+%		\resizebox{1\textwidth}{!}{%
+%			\begin{circuitikz}
+%				\tikzstyle{every node}=[font=\fontsize{14.2pt}{18.5pt}\selectfont]
+%				\draw  (3,12.5) ellipse (2.125cm and 0.625cm);
+%				\node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (3,12.5) {AM-simulation};
+%				\draw  (8.625,13.125) ellipse (2.25cm and 0.625cm);
+%				\node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (8.625,13.125) {HJ-simulation};
+%				\draw  (1.5,10.375) ellipse (1.875cm and 0.625cm);
+%				\node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (1.5,10.375) {F-simulation};
+%				\draw  (6.75,10.625) ellipse (2.75cm and 0.625cm);
+%				\node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (6.75,10.625) {F\comp\appr-simulation};
+%				\draw  (9.625,8) ellipse (2.625cm and 0.625cm);
+%				\node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (9.5,8) {\appr\comp F-simulation};
+%			\end{circuitikz}
+%		}%
+%		\caption{Your Caption}
+%		\label{fig:my_label}
+%	\end{figure}
+%\end{equation}
 %\begin{figure}[t]
 %	\centering
 %	\begin{tabular}{|l|c|c|}
@@ -1962,8 +2289,77 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 %
 %\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{Simulations and Bisimulations in Double Categories}
+\subsection{Abstracting bilax simulation}
+\begin{definition}
+	Given a category $\BC$ with terminal objects, the category $\spa_a(\BC)$ is the category that has all the objects of $\spa(\BC)$, and for $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, there is a  morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ in $\spa_a(\BC)$, whenever the following proposition holds:
+	\begin{gather*}
+		\forall u\in\Hom(1,R),\exists v\in\Hom(1,S),g_1\comp p_1\comp u=q_1\comp v \;\&\;g_2\comp p_2\comp u=q_2\comp v
+	\end{gather*}
+\end{definition}
 %
+\begin{lemma}\label{lem:yoneda}
+	Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have:
+	\begin{gather*}
+		\Hom(X,Y)\iso \Hom(\Hom(A,X),\Hom(A,Y))
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	It is entailed by the Yoneda lemma. The contravariant version of the Yoneda's lemma says that given a functor $G\c\BC^\op\to\Set$ the following correspondance holds:
+	\begin{gather*}
+		GX\iso\Hom(\Hom(\argument,X),G)
+	\end{gather*}
+	If we substitute $G$ with $\Hom(\argument,Y)$ then we have the following:
+	\begin{gather*}
+		\Hom(\argument,Y)\iso\Hom(\Hom(\argument,X),\Hom(\argument,Y))
+	\end{gather*}\qed
+\end{proof}
+%
+\begin{prop}
+	Assuming the axiom of choice, given $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$.
+\end{prop}
+\begin{proof}
+	$(\Rightarrow):$ For every $u\in\Hom(1,R)$ we take $v\in\Hom(1,S)$ to be $w\comp u$.\\
+	$(\Leftarrow):$ Given that $(g_1,g_2)$ is a morphism in $\spa_a(\BC)$ then for every $u\in\Hom(1,R)$ there exists $v\in\Hom(1,S)$ such that $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$. We define a function that takes $u\in\Hom(1,R)$ and gives $V_u\in\powf\Hom(1,S)$ such that for every $v\in V_u$ we have $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$, and $V_u\neq\emptyset$. The axiom of choice gives us a function $s\c\im_h\to\Hom(1,S)$. So, we define a function $k\c\Hom(1,R)\to\Hom(1,S)$ such that $k=s\comp e_h$, where $e_h\c\Hom(1,R)\to\im_h$ is the epimorphism in the image factorization of $h$. By~\autoref{lem:yoneda}, there exists a bijection $\nu\c\Hom(\Hom(1,R),\Hom(1,S))\to\Hom(R,S)$.
+\end{proof}
+%
+\begin{definition}
+	Given a category $\BC$, an endofunctor $F$ over $\BC$ with a natural order structure $\appr$, we call $(FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ a \emph{poset object} over $Y$, whenever for every object $X$ and morphisms $f,g\in\Hom(X,FY)$ such that $f\appr g$, there exists $h\c X\to R_Y$ such that the following diagram commutes:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			FY \& {R_Y} \& FY \\
+			\& X
+			\arrow["{q_1}"', from=1-2, to=1-1]
+			\arrow["{q_2}", from=1-2, to=1-3]
+			\arrow["f", bend left=20, from=2-2, to=1-1]
+			\arrow["h", from=2-2, to=1-2]
+			\arrow["g"', bend right=20, from=2-2, to=1-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
+%
+\begin{definition}[Abstract bi-lax Simlulation]
+	$(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ is an \emph{abstract bi-lax simlulation} from an $F$-coalgebra $(X_1,g_1)$ to $(X_2,g_2)$, whenever there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(FX_1 \stackrel{r_1}{\leftarrow} R_{X_1}\comp FR\comp R_{X_2} \stackrel{r_2}{\to}FX_2)$ in $\spa_a(\BC)$.
+\end{definition}
+%
+\begin{prop}
+	Aczel-Mendler simulation is equivalent with abstract bi-lax simulation under the axiom of choice.
+\end{prop}
+\begin{proof}
+	\todo{Finish!}
+\end{proof}
+%
+\begin{prop}
+	Given a category $\BC$ with pullbacks, then a poset object $(FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ has the following properties:\ppnote{You may need to prove that the witnesses in the following are monic!}\ppnote{I am not even sure if we need this proposition!}
+	\begin{enumerate}
+		\item \emph{Reflexivity:} There is a morphism $(\id_{FY},i,\id_{FY})\c (FY \stackrel{d}{\leftarrow} \Delta_{FY} \stackrel{d}{\to}FY)\to (FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ in $\spa(\BC)$.
+		\item \emph{Antisymmetry:} Given that $(R_Y \stackrel{s_1}{\leftarrow} A \stackrel{s_2}{\to}R_Y)$ is the pullback along $\brks{q_1,q_2}$ and $\brks{q_2,q_1}$, then there is a morphism $(\id_R,i',\id_R)\c (R_Y \stackrel{s_1}{\leftarrow} A \stackrel{s_2}{\to}R_Y)\to (R_Y \stackrel{d'}{\leftarrow} \Delta_R \stackrel{d'}{\to}R_Y)$ in $\spa(\BC)$.
+		\item \emph{Transitivity:} Given that $(R_Y \stackrel{t_1}{\leftarrow} R_Y\comp R_Y \stackrel{t_2}{\to}R_Y)$ is the pullback along $q_1$ and $q_2$, then there is a morphism $(\id_R,i'',\id_R)\c (R_Y \stackrel{t_1}{\leftarrow} R_Y\comp R_Y \stackrel{t_2}{\to}R_Y)\to (R_Y \stackrel{d'}{\leftarrow} \Delta_R \stackrel{d'}{\to}R_Y)$ in $\spa(\BC)$.
+	\end{enumerate} 
+\end{prop}
+%
+
+\section{Simulations and Bisimulations in Double Categories}
+% Given that $(R \stackrel{s_1}{\leftarrow} P \stackrel{s_2}{\to}R)$ is the pullback along $\brks{p_1,p_2}$ and $\brks{p_2,p_1}$, then there is a morphism $(\id_R,i',\id_R)\c (R \stackrel{s_1}{\leftarrow} P \stackrel{s_2}{\to}R)\to (R \stackrel{d'_1}{\leftarrow} \Delta_R \stackrel{d'_2}{\to}R)$ in $\spa(\BC)$.
 %
 %
 \begin{definition}[Double Relator]\label{def:doub-rela}
@@ -2087,13 +2483,13 @@ Given an $F$-relator $\relar$ defined in~\autoref{def:relator} we have a canonic
 	For a category $\BC_0$ with pullbacks and an endofunctor $F$ on it, every abstract relational bisimulation (\autoref{def:abs-rel-bis}) is an $\rel(F)$-double coalgebra that $\rel(F)$ is the map that takes every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to a relation $(FX \stackrel{\rel(F)p_1}{\leftarrow} \rel(F)R \stackrel{\rel(F)p_2}{\to}FY)$. It entails that every Hermida-Jacobs bisimulation is also an $(F-)^\dagger$-double coalgebra if we conceive $(F-)^\dagger$ as the proper double relator.
 \end{example}
 %
+Using the basic fact in $\Set$ that a relation $R\subseteq X\times X$ is a poset iff $R\comp R=R$, we define poset enrichment abstractly as follows:
 \begin{definition}[Poset-enrichment Functor]
-	On a double category $\BC_1\rightrightarrows\BC_0$, for a functor $F\c\BC_0\to\BC_0$ a functor $P_F\c\BC_0\to\BC_1$ is a \emph{poset-enrichment} functor over $F$ such that for every objects $X$ and mrphisms $f$, the following equations hold:
+	On a double category $\BC_1\rightrightarrows\BC_0$, for a functor $F\c\BC_0\to\BC_0$ a functor $P_F\c\BC_0\to\BC_1$ is a \emph{poset-enrichment} functor over $F$ such that for every objects $X$ and mrphisms $f$, the following equations hold ($\Delta$ is the diagonal functor):
 	\begin{gather*}
-		SP_FX=FX,\;TP_FX=FX\\
-		SP_Ff=Ff,\;TP_Ff=Ff\\
-		P_FX=P_FX\odot P_FX\\
-		P_Ff=P_Ff\odot P_Ff
+		SP_F=F\\
+		TP_F=F\\
+		P_F=\odot\comp\Delta\comp P_F
 	\end{gather*}
 \end{definition}
 %
@@ -4334,7 +4730,7 @@ Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a
 	Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
 \end{proof}
 \begin{cor}
-	Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation.
+	Recalling~\autoref{prop:left-lax-inc-triv}, for a functor $F\c\Set\to\Set$, assuming that $F^\leftarrow\leq\bar{F}$, we get $F^\leftarrow=\bar{F}$. So, if $r$ is symmetric, and it is a $F^\leftarrow$-simulation, then it is a $\bar{F}$-bisimulation.ss
 \end{cor}
 \end{document}