only the diagram is left

draft/draft.tex

@@ -725,22 +725,22 @@ From now on, instead of $\spa(\Set)$ and $\rel(\Set)$, we use $\spa$ and $\rel$
 %\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^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that
+	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^\dagger$ as the image of $\brks{p_1,p_2}$ and we take $r\c R\to R^\dagger$ 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.
+	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^\dagger\subseteq X_1\times X_2$ and an bijection $r\c R\to R^\dagger$, such that for every $(x_1,x_2)\in R^\dagger$,
+	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^\dagger$ 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
+	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}
@@ -755,7 +755,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 %		=&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^\dagger$ and $s\c S\to S^\dagger$ 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^\dagger$ we have $(g_1(x_1),g_2(x_2))\in S^\dagger$. So, we define $w'\c R^\dagger\to S^\dagger$ 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:
+	$(\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*}
 		q_i\comp w(u)\\
 		=&q_i\comp s^\mone\comp w'\comp r(u)\\
@@ -786,7 +786,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 \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
@@ -806,7 +806,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
 		$\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$.}
+	\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{notation}
@@ -1233,7 +1233,7 @@ 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]
@@ -1322,11 +1322,11 @@ We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes
 \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:
@@ -1355,14 +1355,34 @@ We can define $(-)^\dagger$ as a functor from $\spa(\BC)\to\rel(\BC)$ that takes
 %\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 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 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 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.\\
+	$(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:
-	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\qed
+	\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}
@@ -1379,9 +1399,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 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 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 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 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.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
+		\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}
@@ -1389,8 +1409,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.\\
+	(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 $(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.
+	($\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 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}
@@ -1452,7 +1472,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
@@ -1466,18 +1486,55 @@ 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 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 $(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 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.}\\
+	$(1)$: 
-	$(2)$: It is obvious using~\autoref{lem:morph-spa-rel}.\sgnote{Add more details.}\qed
+	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}
@@ -1570,19 +1627,20 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 \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 $\tilde{F}$.
+	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 a bi-lax Barr relator of a functor $F$ with $\tilde{F}$.
 \end{example}
 %
 \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 a $\tilde{F}$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ if it is a Hermida-Jacobs simulation.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
+		\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.\ppnote{The proof should be revised with the revision in the definition of $\rel$}
+		\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 $(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 $\tilde{F}$-simulation.\\
+	(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): $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ being a $\tilde{F}$-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
+	
+	(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.
@@ -4450,7 +4508,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}