From 9e1ab1f8ad8b81a400778d6081fae10a151fa5f0 Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 26 Aug 2026 18:56:02 +0100 Subject: [PATCH] bluh --- draft/draft.tex | 54 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/draft/draft.tex b/draft/draft.tex index c82026b..6c8cd7a 100644 --- a/draft/draft.tex +++ b/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]