HeJ and HuJ simulation equivalence

draft/draft.tex

@@ -1114,7 +1114,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
@@ -1128,7 +1128,7 @@ 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}
@@ -1194,22 +1194,24 @@ 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$).
+	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$.
 \end{example}
 %
 \begin{prop}\label{prop:HeJ-HuJ}
-	Every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$:
-	\begin{itemize}
-		\item is a Hughes-Jacobs simulation if it is a Hermida-Jacobs simulation.
-		\item is a Hermida-Jacobs simulation if it is a Hermida-Jacobs simulation, assuming the axiom of choice.
-	\end{itemize}
+	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{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.
+	\end{enumerate}
 \end{prop}
 \begin{proof}
-	\todo{Finish!}
+	(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
 \end{proof}
 \begin{rem}
-	The proposition entails that Hermida-Jacobs simulation subsumes Hughes-Jacobs simulation.
+	The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.
 \end{rem}
+\todo{Read section V of the LICS paper and see what is the non-symmetric relator. Then try to see if HJ-simulation subsumes it.}
 \subsection{Simulations in Double Categories}
 \todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!}
 %We show the category of partially ordered sets with monotone functions between them with $\poset$.