4 defs!

draft/draft.tex

@@ -387,45 +387,51 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
 %
 
 \section{Coalgebraic Bisimulation}%\label{sec:}
-
+In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that at least has products, and by $\rel(\BC)$ we refer to the relatios in $\BC$, and by relation we are referring to a span $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ such that the morphism $\brks{p_1,p_2}$ is a mono. For the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ and $\spa$ we mean $\rel(\Set)$ and $\spa(\Set)$, accordingly.
-\begin{definition}[Relation Lifting]
+%\begin{definition}[Relation Lifting]
-	Assuming $F\c\Set\to\Set$ is a functor, then we call $\rel(F)\c\rel\to\rel$ a relation lifting of $F$, where the following diagram commutes:
+%	Assuming $F\c\BC\to\BC$ is a functor, then we call $\rel(F)\c\rel(\BC)\to\rel(\BC)$ a relation lifting of $F$, where the following diagram commutes:
-	\begin{equation*}
+%	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
+%		\begin{tikzcd}[ampersand replacement=\&]
-			\rel \&\& \rel \\
+%			\rel(\BC) \&\& \rel(\BC) \\
-			{\Set\times\Set} \&\& {\Set\times\Set}
+%			{\BC\times\BC} \&\& {\BC\times\BC}
-			\arrow["{\rel(F)}", from=1-1, to=1-3]
+%			\arrow["{\rel(F)}", from=1-1, to=1-3]
-			\arrow[from=1-1, to=2-1]
+%			\arrow[from=1-1, to=2-1]
-			\arrow[from=1-3, to=2-3]
+%			\arrow[from=1-3, to=2-3]
-			\arrow["{F\times F}"', from=2-1, to=2-3]
+%			\arrow["{F\times F}"', from=2-1, to=2-3]
-		\end{tikzcd}
+%		\end{tikzcd}
-	\end{equation*}
+%	\end{equation*}
+%\end{definition}
+%We have notions of bisimulation that may involve relation lifting. An example of relation lifting is to use the image factorization provided in regular categories. 
+\begin{definition}[$F$-Relator]
+	For a set functor $F$, and for sets $X$ and $Y$, an $F$-relator $\relar$ is a map that takes every relation on $X\times Y$ to a relation on $FX\times FY$, and it is monotone with respect to inclusion.
 \end{definition}
+%Also, for the time being, we limit the discussion to the case $\BC=\Set$. For simplicity, by $\rel$ we mean $\rel(\BC)$.
 %
-We take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $F$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$.
+%We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F$ takes a relation $R$, where $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and gives the relation that is the image of the function $\brks{Fp_1,Fp_2}\c FR\to FX\times FY$.
-\begin{definition}[Bisimulation]
+%\begin{definition}[Bisimulation]
-	For a functor $F\c\Set\to\Set$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
+%	For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
-\end{definition}
+%\end{definition}
 %
-\begin{prop}
+%\begin{prop}
-	Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\Set\times\Set$, then the following diagram commutes, and vice-versa:
+%	Assuming that $(R,\alpha)$ is a $\rel(F)$-coalgebra, where $\alpha=\beta_1\times\beta_2$ in $\BC\times\BC$, then the following diagram commutes, and vice-versa:
-	\begin{equation*}
+%	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
+%		\begin{tikzcd}[ampersand replacement=\&]
-			{X_1} \& R \& {X_2} \\
+%			{X_1} \& R \& {X_2} \\
-			{FX_1} \& FR \& {FX_2}
+%			{FX_1} \& FR \& {FX_2}
-			\arrow["{\beta_1}"', from=1-1, to=2-1]
+%			\arrow["{\beta_1}"', from=1-1, to=2-1]
-			\arrow["{p_1}"', from=1-2, to=1-1]
+%			\arrow["{p_1}"', from=1-2, to=1-1]
-			\arrow["{p_2}", from=1-2, to=1-3]
+%			\arrow["{p_2}", from=1-2, to=1-3]
-			\arrow["\beta", from=1-2, to=2-2]
+%			\arrow["\beta", from=1-2, to=2-2]
-			\arrow["{\beta_2}", from=1-3, to=2-3]
+%			\arrow["{\beta_2}", from=1-3, to=2-3]
-			\arrow["{Fp_1}", from=2-2, to=2-1]
+%			\arrow["{Fp_1}", from=2-2, to=2-1]
-			\arrow["{Fp_2}"', from=2-2, to=2-3]
+%			\arrow["{Fp_2}"', from=2-2, to=2-3]
-		\end{tikzcd}
+%		\end{tikzcd}
-	\end{equation*}
+%	\end{equation*}
-\end{prop}
+%\end{prop}
 
 \begin{definition}[Aczel-Mendler Bisimulation]
-	\begin{equation*}
+	A relation $R\subseteq X\times Y$ is an \emph{Aczel-Mendler bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to FR$ called witness that commutes in the following diagram:
+	\begin{equation*}\label{eq:acz-mend-diag}
 		\begin{tikzcd}[ampersand replacement=\&]
 			{X} \& R \& {Y} \\
 			{FX} \& FR \& {FY}
@@ -440,51 +446,72 @@ We take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $
 	\end{equation*}
 \end{definition}
 
-\begin{definition}[Hermida-Jacobs Bisimulation]
+\begin{definition}[Witnessless $\relar$-Bisimulation]
+	For a relator $\relar$, a relation $R\subseteq X\times Y$ is a \emph{witnessless $\relar$-bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(\relar R)}\beta(y)$.
+%	\begin{equation*}
+%		\begin{tikzcd}[ampersand replacement=\&]
+%			{X} \& R \& {Y} \\
+%			{FX} \& \rel(F)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["{\beta}", from=1-3, to=2-3]
+%			\arrow["{q_1}", from=2-2, to=2-1]
+%			\arrow["{q_2}"', from=2-2, to=2-3]
+%		\end{tikzcd}
+%	\end{equation*}
+\end{definition}
+
+\begin{definition}[Witnessful $\relar$-Bisimulation]
+	For a relator $\relar$, a relation $R\subseteq X\times Y$ is a \emph{witnessful $\relar$-bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever there is a morphism $\gamma\c R\to \relar R$ called witness that commutes in the following diagram:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			{X} \& R \& {Y} \\
-			{FX} \& (FR)^\dagger \& {FY}
+			{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["\gamma", from=1-2, to=2-2]
 			\arrow["{\beta}", from=1-3, to=2-3]
-			\arrow["{(Fp_1)^\dagger}", from=2-2, to=2-1]
+			\arrow["{q_1}", from=2-2, to=2-1]
-			\arrow["{(Fp_2)^\dagger}"', from=2-2, to=2-3]
+			\arrow["{q_2}"', from=2-2, to=2-3]
-		\end{tikzcd}
-	\end{equation*}
-\end{definition}
-
-\begin{definition}[Hughes-Jacobs Bisimulation]
-	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
-			{X} \& R \& {Y} \\
-			{FX} \& (FR)^\dagger \& {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["{\beta}", from=1-3, to=2-3]
-			\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{definition}
 
 \begin{definition}[Vanilla Bisimulation]
-	\begin{equation*}
+	A relation $R\subseteq X\times Y$ is a \emph{vanilla bisimulation} from an $F$-coalgebra $(X,\alpha)$ to an $F$-coalgebra $(Y,\beta)$ whenever for every $x\in X$ and $y\in Y$, we have $x\mathrel{R} y\Rightarrow \alpha(x)\mathrel{(FR)}\beta(y)$.
-		\begin{tikzcd}[ampersand replacement=\&]
+%	\begin{equation*}
-			{X} \& R \& {Y} \\
+%		\begin{tikzcd}[ampersand replacement=\&]
-			{FX} \& FR \& {FY}
+%			{X} \& R \& {Y} \\
-			\arrow["{\alpha}"', from=1-1, to=2-1]
+%			{FX} \& FR \& {FY}
-			\arrow["{p_1}"', from=1-2, to=1-1]
+%			\arrow["{\alpha}"', from=1-1, to=2-1]
-			\arrow["{p_2}", from=1-2, to=1-3]
+%			\arrow["{p_1}"', from=1-2, to=1-1]
-			\arrow["{\beta}", from=1-3, to=2-3]
+%			\arrow["{p_2}", from=1-2, to=1-3]
-			\arrow["{Fp_1}", from=2-2, to=2-1]
+%			\arrow["{\beta}", from=1-3, to=2-3]
-			\arrow["{Fp_2}"', from=2-2, to=2-3]
+%			\arrow["{Fp_1}", from=2-2, to=2-1]
-		\end{tikzcd}
+%			\arrow["{Fp_2}"', from=2-2, to=2-3]
-	\end{equation*}
+%		\end{tikzcd}
+%	\end{equation*}
 \end{definition}
+\begin{prop}
+	The following propositions hold:
+	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
+		\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
+		\item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
+		\item Every Aczel-Mendler bisimulation is a witnessful bisimulation.
+		\item Assuming the axiom of choice, every witnessful bisimulation is an Aczel-Mendler bisimulation.
+		\item Every witnessless bisimulation is a witnessful bisimulation.
+		\item Assuming the axiom of choice, every witnessless bisimulation is a witnessful bisimulation. 
+	\end{enumerate}
+\end{prop}
+\begin{proof}
+	(I): Assuming $x\mathrel{R}y$, then given by~\eqref{eq:acz-mend-diag} we have $\gamma(x,y)\in FR$, $Fp_1\comp\gamma(x,y)=\alpha(x)$, and $Fp_2\comp\gamma(x,y)=\beta(y)$ that means $\alpha(x)\mathrel{(FR)}\beta(y)$.
+	
+	(II): Since $R$ is a vanilla bisimulation, for every $(x,y)\in R$ we have $\alpha(x)\mathrel{(FR)}\beta(y)$, so we can define $\gamma\c R\to FR$ as $\gamma(x,y)=(\alpha(x),\beta(y))$, and then $\gamma$ commutes in~\eqref{eq:acz-mend-diag}.
+	
+	(III):
+\end{proof}
 \todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
 
 \todo{In next section run a similar analysis for simulation: relator-based vs. Aczel-Mendler.}