todo

draft/draft.tex

@@ -1178,7 +1178,7 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 %\end{definition}
 
 \begin{definition}[Relator-based Simulation]
-	Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if there is a morphism in $\rel$ from $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$, i.e, if $(x,y)\in R$ entails $(\alpha(x),\beta(y))\in\relar R$, for all $x\in X$ and $y\in Y$.
+	Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if there is a morphism in $\rel_a$ from $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \relar R \stackrel{q_2}{\to}FY)$, i.e, if $(x,y)\in R$ entails $(\alpha(x),\beta(y))\in\relar R$, for all $x\in X$ and $y\in Y$.
 \end{definition}
 %
 \begin{definition}[Symmetric Relator]
@@ -1196,8 +1196,22 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
 \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$).
 \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}
+\end{prop}
+\begin{proof}
+	\todo{Finish!}
+\end{proof}
+\begin{rem}
+	The proposition entails that Hermida-Jacobs simulation subsumes Hughes-Jacobs simulation.
+\end{rem}
 \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$. 
 %\begin{definition}[A Partial Order Over a Functor]
 %	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes: