bluh

draft/draft.tex

@@ -285,6 +285,7 @@
 \newcommand{\preord}{\mathbf{PreOrd}}
 \newcommand{\poset}{\mathbf{PoSet}}
 \newcommand{\rel}{\mathbf{Rel}}
+\newcommand{\rels}{\mathbf{RelSet}}
 \newcommand{\spa}{\mathbf{Span}}
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
@@ -1142,7 +1143,60 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
 \end{proof}
 %
 \subsection{Simulations in Set}
+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$.
+%\end{notation}
+%\begin{lemma}\label{lem:set-rel-span-equiv}
+%	$R\c X\rto Y$ is a morphism in $\rels$ iff there is an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$.
+%\end{lemma}
+%\begin{proof}
+%	($\Rightarrow$): $R\c X\rto Y$ being a morphism in $\rels$ means that in $\Set$ there exist an object $R$ with a unique mono of type $R\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an object in $\rel$.
+%	
+%	($\Leftarrow$): If $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an object in $\rel$, then $R$ is a binary relation from $X$ to $Y$ so, it is a morphism of type $X\rto Y$ in $\rels$.\qed
+%\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]
+	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)$. 
+\end{definition}
+%
+%\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim-rela}
+%	For a relator $\relar$ on a functor $F$ a HJ-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
+%	\begin{equation}\label{eq:hej-sim}
+%		\begin{tikzcd}[ampersand replacement=\&]
+%			X \& r \& Y \\
+%			{FX} \& {\relar r} \& {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["{{(Fp_1)}^\relar}", from=2-2, to=2-1]
+%			\arrow["{{(Fp_2)}^\relar}"', from=2-2, to=2-3]
+%		\end{tikzcd}
+%	\end{equation}
+%\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$.
+\end{definition}
+%
+\begin{definition}[Symmetric Relator]
+	A relator $\relar$ is symmetric if and only if for every relation $R$ we have $\relar(R^\op)=(\relar R)^\op$.
+\end{definition}
+%
+\begin{definition}[Relator-based Bisimulation]
+	Given a relator $\relar$, a relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is an $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ whenever $R$ is an $\relar$-simulation, and $\relar$ is a symmetric relator.
+\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.
+\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$).
+\end{example}
+\subsection{Simulations in Double Categories}
 
 %We show the category of partially ordered sets with monotone functions between them with $\poset$. 
 %\begin{definition}[A Partial Order Over a Functor]