minor

draft/draft.tex

@@ -1454,19 +1454,19 @@ 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 $F^\leftrightarrow$.
+	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}$.
 \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)$:
+	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 a coalgebra $(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.
+		\item is a $\tilde{F}$-simulation if it is a Hermida-Jacobs simulation.
+		\item is a Hermida-Jacobs simulation 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 $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
+	(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.\\
+	(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
 \end{proof}
 \begin{rem}
 	The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators.