misc feedback

draft/draft.tex

@@ -388,8 +388,14 @@ 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 category of relations 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. We show morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
+In this section, by $\spa(\BC)$ we refer to spans in a category $\BC$ that has
-A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\BC)$), whenever $f$, $g_1$ and $g_2$ are morphisms in $\BC$ for which the following diagram commutes in $\BC$: 
+products, and by $\rel(\BC)$ we refer to the category of relations in $\BC$, i.e.\
+such spans $(X \stackrel{p_1}{\leftarrow} R
+\stackrel{p_2}{\to}Y)$ that the morphism $\brks{p_1,p_2}$ is a mono.
+We denote morphisms in $\spa(\BC)$ by $\spto$, and in $\rel(\BC)$ by $\rto$.
+A morphism $R\rto S$ ($R\spto S$) in $\rel(\BC)$
+($\spa(\BC)$) is such a triple of morphisms $(f\c R\to S, g_1\c X_1\to Y_1, g_2\c X_2\to Y_2)$ 
+in $\BC$ that the following diagram commutes:
 	\begin{equation*}
 		\begin{tikzcd}[ampersand replacement=\&]
 			{X_1} \& R \& {X_2} \\
@@ -417,8 +423,9 @@ A morphism $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel(\BC)$ ($\spa(\B
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}	
-
+%
-We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is to use the image factorization provided in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
+We have notions of bisimulation that may involve relation lifting. An example of a relation lifting is obtained 
+by the image factorization in regular categories. \ppnote{Initially, I wanted to give the definitions for an arbitrary relation lifting. I think it can be doable, but for simplicity I preferred to stick to this one.}
 %
 %\begin{equation*}
 %	\begin{tikzcd}[ampersand replacement=\&]
@@ -450,13 +457,33 @@ So, for every functor $F\c\BC\to\BC$ we have $(F-)^\dagger\c\rel(\BC)\to\rel(\BC
 		\arrow["{{\brks{{(Fp_1)^\dagger},{(Fp_2)^\dagger}}}}"{description}, dashed, tail, from=1-2, to=3-2]
 	\end{tikzcd}
 \end{equation*}
-
+%
-Also, there exist a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. 
+%There exists a well-known notion named relator, instead of relation lifting. A relator does not need to be a functor, but it should be a map of a specific type format that is monotone with respect to inclusion. Also, relators are defined only on $\Set$ unlike relation liftings. %We discuss relators more in depth in the later chapters. 
 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.
 
-In $\Set$, there is another way to define the morphisms that is to say that $f\c R\rto S$ ($f\c R\spto S$) is a morphism in $\rel$ ($\spa$), whenever there are functions $g_1$ and $g_2$ that $x\mathrel{R}y\Rightarrow g_1(x)\mathrel{(FR)}g_2(y)$. 
+We can define morphisms in $\rel$ differently by only requesting such functions $g_1$ and $g_2$ that $x\mathrel{R}y$ entails $g_1(x)\mathrel{S}g_2(y)$. Let us 
+call such morphisms \emph{anonymous} (because they omit the witnessing part $f$, which is unique for relations but not for general spans). This however yields 
+an equivalent definition. \todo{Add a proof.} \todo{Do the same for spans; prove equivalence under the axiom of choice.}
+
+By varying from anonymous to non-anonymous morphisms and from $\rel$ to $\spa$ we 
+can obtain for flavors of bisimulation (\autoref{eq:acz-mend-diag}--\autoref{def:vanila}) -- 
+\autoref{fig:anonymous_onymous} contains a comprehensible summary.
+
+\begin{figure}[t]
+\centering
+\begin{tabular}{|l|c|c|}
+\hline
+ & \textbf{Anonymous} & \textbf{Onymous} \\
+\hline
+\textbf{Relations} & Witnessless & Hermida-Jacobs \\
+\hline
+\textbf{Spans} & Vanilla & Aczel-Mendler \\
+\hline
+\end{tabular}
+\caption{Comparison of anonymous and onymous settings for relations and spans.}
+\label{fig:anonymous_onymous}
+\end{figure}
 
-Now, considering the two types of morphisms that we can define for $\rel$, and having lifting over the relation or not, we give four notions of bisimulation:
 %We take $\rel(F)\c\rel(\BC)\to\rel(\BC)$ to be the functor that for an arbitrary functor $F\c\BC\to\BC$ 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]
 %	For a functor $F\c\BC\to\BC$, a bisimulation is a $\rel(F)$-coalgebra in $\rel$.
@@ -484,6 +511,9 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h
 %	\end{equation*}
 %\end{prop}
 \begin{definition}[Aczel-Mendler Bisimulation]
+\todo{Explain in terms of span morphisms}. 
+
+
 	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=\&]
@@ -499,8 +529,10 @@ Now, considering the two types of morphisms that we can define for $\rel$, and h
 		\end{tikzcd}
 	\end{equation*}
 \end{definition}
-Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$ instead of $\Set$. Worth noting that with this definition,if $R$ is a bisimulation, it does not necassirily mean that $FR$ is a relation as well, for example $FR$ can have elements that are not pairs.  
+Aczel-Mendler bisimulation can be defined for an arbitrary category $\BC$
-
+instead of $\Set$. It is worth noting that with this definition, if $R$ is a
+relation, it does not necassirily mean that $FR$ is a relation as well.
+%
 \begin{definition}[Witnessless Bisimulation]
 	A relation $R\subseteq X\times Y$ is a \emph{witnessless 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)^\dagger}\beta(y)$.
 %	\begin{equation*}
@@ -536,7 +568,7 @@ A more general version of witnessless bisimulation is given by Hughes and Jacobs
 \end{definition}
 Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary category $\BC$.
 
-\begin{definition}[Vanilla Bisimulation]
+\begin{definition}[Vanilla Bisimulation]\label{def:vanila}
 	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{equation*}
 %		\begin{tikzcd}[ampersand replacement=\&]
@@ -554,6 +586,7 @@ Hermida-Jacobs bisimulation is also traditionally defined for an arbitrary categ
 We do not know if this definition exists anywhere.
 \begin{prop}
 	The following propositions hold in $\Set$:
+	\todo{How about proving that 1.3,1.4,1.5 are equivalent to each other, and all together to 1.2 under axiom of choice? }
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
 		%\item Every Aczel-Mendler bisimulation is a vanilla bisimulation.
 		\item Every vanilla bisimulation is an Aczel-Mendler bisimulation.
@@ -574,13 +607,12 @@ We do not know if this definition exists anywhere.
 	
 	(IV): Similar to (I) we can define $\gamma(x,y)=(\alpha(x),\beta(y))$ as the witness for $R$ to be a Hermida-Jacobs bisimulation.  
 \end{proof}
-\begin{rem}
+\begin{rem}\todo{No, these definitions are just equivalent.}
 	For vanilla bisimulation to be a witnessless bisimulation (or vice-versa) for a relation $R$ we need to have $FR\subseteq (FR)^\dagger$ (or $(FR)^\dagger\subseteq FR$), which is rarely true. The condition may not even be true for other relation liftings for these functors.
 \end{rem}
 \begin{rem}
+\todo{No, this does not follow from anythying.}   
 	To have an Aczel-Mendler bisimulation to be a vanilla bisimulation we need to have $FR\subseteq FX\times FY$ that is a rare condition. It does not hold for powerset functor or maybe functor.
-	
-	To have a Hermida-Jacobs bisimulation to be a witnessless bisimulation we need to have $(FR)^\dagger\subseteq FX\times FY$ that is more common, for example it is true for the powerset functor, although we still can not prove it for the general case. Perhaps a condition is needed to be able to have a general statement.
 \end{rem}
 \todo{Discuss 4 versions of bisimulation (with witness/without witness, for relations/for spans). Which are equivalent? Which do not make sense?}
 
@@ -2005,33 +2037,36 @@ We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest a
 %\end{proof}
 \subsection{The concrete proof}
 \begin{lemma}\label{lem:sim-opsim-inc}
-	Assuming that $\sigma\c R\to\powf R$ is witness for the symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
+	Assuming that $\sigma\c R\to\powf R$ is witness for a symmetric relation $R$ to be an AM simulation on $\powf$-coalgebra $(X,\alpha)$, then for all $(x_1,x_2)\in R$ we have:
 	\begin{enumerate}[label=(\Roman*), ref=(\Roman*)]
 		\item $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$\label{item:sim-opsim-inc:I}
 		\item $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$\label{item:sim-opsim-inc:II}
 	\end{enumerate}
 \end{lemma}
 \begin{proof}
-	By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
+	 By~\eqref{eq:diag-lax-sim} for every $(x_1,x_2)\in R$ we have
-	\begin{gather*}
+	\begin{align}
-		\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2),\\
+		\alpha(x_1)\subseteq&\;\powf p_1\comp\sigma(x_1,x_2),\label{eq:alpha_x_1}\\
-		\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2).
+		\powf p_2\comp\sigma(x_1,x_2)\subseteq&\;\alpha(x_2).\label{eq:alpha_x_2}
-	\end{gather*}
+	\end{align}
-	Since $R$ is symmetric $(x_2,x_1)\in R$, so from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$, where 
+	(I): Since $R$ is symmetric $(x_2,x_1)\in R$, so from \eqref{eq:alpha_x_2} we get $\powf p_2\comp\sigma(x_2,x_1)\subseteq\alpha(x_1)$. 
+	Therefore:
 	\begin{align*}
-		\powf p_2\comp\sigma(x_2,x_1)&\\
+	\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)=&\; \powf p_2\comp\sigma\comp s(x_1,x_2)\\
-		&=\powf p_2\comp\sigma\comp s(x_1,x_2)\\
+	=&\; \powf p_2\comp\sigma (x_2,x_1)\\
-		&=\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2).
+	\subseteq&\;\alpha(x_1)\\
+	\subseteq&\; \powf p_1\comp\sigma(x_1,x_2) & \by{\eqref{eq:alpha_x_1}}
 	\end{align*}
-	So, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ we have $\powf p_1\comp\powf s\comp\sigma\comp s(x_1,x_2)\subseteq \powf p_1\comp\sigma(x_1,x_2)$.
+	%
-	
+	(II): Analogously, from~\eqref{eq:alpha_x_1} by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$.
-	Furthermore, from $\alpha(x_1)\subseteq\powf p_1\comp\sigma(x_1,x_2)$ by the symmetry of $R$ we have $(x_2,x_1)\in R$, so we get $\alpha(x_2)\subseteq\powf p_1\comp\sigma(x_2,x_1)$, where 
+	Therefore:
 	\begin{align*}
-		\powf p_1\comp\sigma(x_2,x_1)&\\
+	\powf p_2\comp\sigma(x_1,x_2)\subseteq&\; \alpha(x_2) &\by{\eqref{eq:alpha_x_2}}\\
-		&=\powf p_1\comp\sigma\comp s(x_1,x_2)\\
+	\subseteq&\; \powf p_1\comp\sigma(x_2,x_1) \\
-		&=\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).
+	=&\; \powf p_1\comp\sigma\comp s(x_1,x_2) \\
+	=&\;\powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2).& 
 	\end{align*}
-	So, from $\powf p_2\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ we have $\powf p_2\comp\sigma(x_1,x_2)\subseteq \powf p_2\comp\powf s\comp\sigma\comp s(x_1,x_2)$.\qed
+	\qed
 \end{proof}
 We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
 \begin{gather*}
@@ -2073,12 +2108,12 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$:
 %	Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation.
 %\end{rem}
 Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut.
-\begin{lemma}\label{lem:alph-prod}
+\begin{prop}\label{lem:alph-prod}
-	Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$. 
+	Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then there exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, such that $\powf p_1\comp\sigma'=\alpha\comp p_1$. 
-\end{lemma}
+\end{prop}
 \begin{proof}
 	We define $\sigma'(x_1,x_2)=\{(x'_1,x'_2)\mid x'_1\in\alpha\comp p_1(x_1,x_2)\;,\;(x'_1,x'_2)\in\sigma(x_1,x_2)\}$. We have $\sigma'\subseteq\sigma$ that gives $\powf p_2\comp\sigma'\subseteq\powf p_2\comp\sigma$. Additionally, we have $\powf p_1\comp\sigma'\subseteq\alpha\comp p_1$.
-	Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$, which means that exists $x'_2$ that $(x'_1,x'_2)\in\sigma(x_1,x_2)$. So, by definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. 
+	Furthermore, if $x'_1\in\alpha\comp p_1(x_1,x_2)$, since $\alpha\comp p_1\subseteq \powf p_1\comp\sigma$ then $x'_1\in\powf p_1\comp\sigma(x_1,x_2)$. Let $(x'_1,x'_2)\in\sigma(x_1,x_2)$. By definition of $\sigma'$, we have $(x'_1,x'_2)\in\sigma'(x_1,x_2)$, so $x'_1\in\powf p_1\comp\sigma'(x_1,x_2)$ that means $\alpha\comp p_1\subseteq \powf p_1\comp\sigma'$ as well. So, $\sigma'$ is another witness for $R$ to be an AM simulation, and we have $\alpha\comp p_1=\powf p_1\comp\sigma'$. 
 	\qed
 \end{proof}
 \begin{prop}\label{prop:sym-rel-bisim}
@@ -2088,12 +2123,13 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the
 	\end{gather*}
 \end{prop}
 \begin{proof}
-	For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:I} we have 
+	For every $(x_1,x_2)\in R$ by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:I} we have 
 	\begin{gather*}
 		\powf p_1\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
-		\powf p_1\comp\sigma(x_1,x_2),
+		\powf p_1\comp\sigma(x_1,x_2).
 	\end{gather*}
-	and by~\autoref{lem:alph-prod}, $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. Furthermore, by~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\eqref{item:sim-opsim-inc:II} we have
+%	and by~\autoref{lem:alph-prod}, 
+	Recall that $\powf p_1\comp\sigma(x_1,x_2)=\alpha(x_1)$. By~\autoref{lem:proj-dist-set} and~\autoref{lem:sim-opsim-inc}.\ref{item:sim-opsim-inc:II} we have
 	\begin{gather*}
 		\powf p_2\comp(\sigma\join(\powf s\comp\sigma\comp s))(x_1,x_2)=
 		\powf p_2\comp(\powf s\comp\sigma\comp s)(x_1,x_2).