Merge branch 'master' of git.wlog.site:pouya/coalgebraic-simulation

draft/draft.tex

@@ -385,22 +385,9 @@ Pouya Partow\inst{1}\orcidID{0009-0003-9652-9469}}
 \end{abstract}
 %
 %
-%
-\section{Coalgebraic Simulation}
-We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
-\begin{definition}[A Preorder Over a Functor]
-	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes:
-	\begin{equation*}
-		\begin{tikzcd}[ampersand replacement=\&]
-			\& \preord \\
-			\Set \& \Set
-			\arrow[from=1-2, to=2-2]
-			\arrow["\appr", from=2-1, to=1-2]
-			\arrow["F"', from=2-1, to=2-2]
-		\end{tikzcd}
-	\end{equation*}
-\end{definition}
-%
+
+\section{Coalgebraic Bisimulation}%\label{sec:}
+
 \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:
 	\begin{equation*}
@@ -436,6 +423,29 @@ We take $\rel(F)\c\rel\to\rel$ to be the functor that for an arbitrary functor $
 		\end{tikzcd}
 	\end{equation*}
 \end{prop}
+
+
+\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.}
+
+%
+\section{Coalgebraic Simulation}
+We show the category of preorders with monotone functions between them with $\preord$. In the diagrams, any arrow that shows a functor, but does not have a label is showing a forgetful functor. Also, we use $\rel$ to refer to the category of binary relations. Assuming $R\in\obj(\rel)$ and $R\subseteq X_1\times X_2$, and $S\in\obj(\rel)$ and $S\subseteq Y_1\times Y_2$, then a morphism $f\c R\to S$ in this category is the pair $(f_1,f_2)$ of morhpisms in $\Set$, where, $f_1\c X_1\to Y_1$ and $f_2\c X_2\to Y_2$, and for each $(x_1,x_2)\in R$ we have $(f_1(x_1),f_2(x_2))\in S$. Also, we show projections of $R\in\obj(\rel)$ with $p_1$ and $p_2$ that are morphisms in $\Set$.
+\begin{definition}[A Preorder Over a Functor]
+	Assuming $F\c\Set\to\Set$ is a functor, we call $\appr\c\Set\to\preord$ an order over the functor $F$ iff the following diagram commutes:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			\& \preord \\
+			\Set \& \Set
+			\arrow[from=1-2, to=2-2]
+			\arrow["\appr", from=2-1, to=1-2]
+			\arrow["F"', from=2-1, to=2-2]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
+%
+
 We gave an introduction to Hughes and Jacobs paper. They also have a way to represent simulation relations. In the following, we try to find a suitable formalization for simulation relations, inspired by Hughes and Jacobs.
 \subsection{Relations as \cancel{Pullbacks} Spans(?)}
 We can not show every relation by pullbacks, but we can just show relations of the form
@@ -1036,6 +1046,7 @@ We show this relation with $F_\rel(R,X)$.
 		\end{tikzcd}
 	\end{equation}
 \end{definition}
+\todo{Prove that simulation in this sense of this definition is a standard simulation for powerset.}
 \begin{definition}[Bisimulation]\label{def:bisim}
 	The morphism $\sigma$ in~\autoref{def:sim} is a bisimulation iff the mentioned diagram is fully commutative.
 \end{definition}
@@ -1626,6 +1637,7 @@ Then we have
 	\end{tikzcd}
 \end{equation*}
 We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest are simulations.
+\todo{So, $\sigma_3$ is a unique witness of bisimulation. How can we characterize it among all witnesses of simulation.}
 \begin{definition}\label{def:join-meet}
 We define $\join$ and $\meet$ on morphisms as follows:
 \begin{gather*}