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

draft/draft.tex

@@ -704,9 +704,9 @@ Now, we prove $Sg(\mu') = \nu$.
 \begin{definition}[Category of Relations]
 For an arbitrary category $\BC$, the category of relations, denoted by $\rel(\BC)$ is a full subcategory of $\spa(\BC)$ such that for every object $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ in $\rel(\BC)$, $p_1$ and $p_2$ are jointly monic. %A morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to (Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ is a morphism in $\rel(\BC)$ as well, whenever both $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ are objects in $\rel(\BC)$ as well, and $g_1$ and $g_2$ are jointly monic.
 \end{definition}
-\begin{remark}
-	Followed by~\autoref{prop:joint-mon-unique}, given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel(\BC)$, for morphisms $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$ in $\BC$, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then for every $v\c R\to S$, such that $(g_1,g_2,v)$ is a morphism in $\rel(\BC)$, then $v=w$. 
-\end{remark}
+%\begin{remark}
+%	Followed by~\autoref{prop:joint-mon-unique}, given objects $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\rel(\BC)$, for morphisms $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$ in $\BC$, if there is a morphism $(g_1,g_2,w)\c (X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ then for every $v\c R\to S$, such that $(g_1,g_2,v)$ is a morphism in $\rel(\BC)$, then $v=w$. 
+%\end{remark}
 %
 %\begin{prop}
 %	Assuming that $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, are objects existing in both categories $\rel(\BC)$ and $\spa(\BC)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morhpism $(g_1,g_2,w)$ of the same type in $\rel(\BC)$.
@@ -2289,8 +2289,77 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 %
 %\subsection{Choosing a suitable order for our setting}
 %Maybe we can first choose a suitable order on $T(\Sigma_\val\mS\times D(\mS,\mS))$ and then prove that if a relation and its inverse is a simulation then it is a bisimulation as well. Maybe $T$ being $\omega$-continuous can give the ordering. It can be something easier that relates to termination as well! That if a term has a big-step evaluation, then it is bigger than or equal to any other term, and if it does not, then it is less than or equal to any other term.
-\section{Simulations and Bisimulations in Double Categories}
+\subsection{Abstracting bilax simulation}
+\begin{definition}
+	Given a category $\BC$ with terminal objects, the category $\spa_a(\BC)$ is the category that has all the objects of $\spa(\BC)$, and for $g_1\c X_1\to Y_1$ and $g_2\c X_2\to Y_2$, there is a  morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ in $\spa_a(\BC)$, whenever the following proposition holds:
+	\begin{gather*}
+		\forall u\in\Hom(1,R),\exists v\in\Hom(1,S),g_1\comp p_1\comp u=q_1\comp v \;\&\;g_2\comp p_2\comp u=q_2\comp v
+	\end{gather*}
+\end{definition}
 %
+\begin{lemma}\label{lem:yoneda}
+	Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have:
+	\begin{gather*}
+		\Hom(X,Y)\iso \Hom(\Hom(A,X),\Hom(A,Y))
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	It is entailed by the Yoneda lemma. The contravariant version of the Yoneda's lemma says that given a functor $G\c\BC^\op\to\Set$ the following correspondance holds:
+	\begin{gather*}
+		GX\iso\Hom(\Hom(\argument,X),G)
+	\end{gather*}
+	If we substitute $G$ with $\Hom(\argument,Y)$ then we have the following:
+	\begin{gather*}
+		\Hom(\argument,Y)\iso\Hom(\Hom(\argument,X),\Hom(\argument,Y))
+	\end{gather*}\qed
+\end{proof}
+%
+\begin{prop}
+	Assuming the axiom of choice, given $(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ and $(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$, there is a morphism $(g_1,g_2,w)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$ iff there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(Y_1 \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Y_2)$ in $\spa(\BC)$.
+\end{prop}
+\begin{proof}
+	$(\Rightarrow):$ For every $u\in\Hom(1,R)$ we take $v\in\Hom(1,S)$ to be $w\comp u$.\\
+	$(\Leftarrow):$ Given that $(g_1,g_2)$ is a morphism in $\spa_a(\BC)$ then for every $u\in\Hom(1,R)$ there exists $v\in\Hom(1,S)$ such that $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$. We define a function that takes $u\in\Hom(1,R)$ and gives $V_u\in\powf\Hom(1,S)$ such that for every $v\in V_u$ we have $g_1\comp p_1\comp u=q_1\comp v$ and $g_2\comp p_2\comp u=q_2\comp v$, and $V_u\neq\emptyset$. The axiom of choice gives us a function $s\c\im_h\to\Hom(1,S)$. So, we define a function $k\c\Hom(1,R)\to\Hom(1,S)$ such that $k=s\comp e_h$, where $e_h\c\Hom(1,R)\to\im_h$ is the epimorphism in the image factorization of $h$. By~\autoref{lem:yoneda}, there exists a bijection $\nu\c\Hom(\Hom(1,R),\Hom(1,S))\to\Hom(R,S)$.
+\end{proof}
+%
+\begin{definition}
+	Given a category $\BC$, an endofunctor $F$ over $\BC$ with a natural order structure $\appr$, we call $(FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ a \emph{poset object} over $Y$, whenever for every object $X$ and morphisms $f,g\in\Hom(X,FY)$ such that $f\appr g$, there exists $h\c X\to R_Y$ such that the following diagram commutes:
+	\begin{equation*}
+		\begin{tikzcd}[ampersand replacement=\&]
+			FY \& {R_Y} \& FY \\
+			\& X
+			\arrow["{q_1}"', from=1-2, to=1-1]
+			\arrow["{q_2}", from=1-2, to=1-3]
+			\arrow["f", bend left=20, from=2-2, to=1-1]
+			\arrow["h", from=2-2, to=1-2]
+			\arrow["g"', bend right=20, from=2-2, to=1-3]
+		\end{tikzcd}
+	\end{equation*}
+\end{definition}
+%
+\begin{definition}[Abstract bi-lax Simlulation]
+	$(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)$ is an \emph{abstract bi-lax simlulation} from an $F$-coalgebra $(X_1,g_1)$ to $(X_2,g_2)$, whenever there is a morphism $(g_1,g_2)\c(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)\to(FX_1 \stackrel{r_1}{\leftarrow} R_{X_1}\comp FR\comp R_{X_2} \stackrel{r_2}{\to}FX_2)$ in $\spa_a(\BC)$.
+\end{definition}
+%
+\begin{prop}
+	Aczel-Mendler simulation is equivalent with abstract bi-lax simulation under the axiom of choice.
+\end{prop}
+\begin{proof}
+	\todo{Finish!}
+\end{proof}
+%
+\begin{prop}
+	Given a category $\BC$ with pullbacks, then a poset object $(FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ has the following properties:\ppnote{You may need to prove that the witnesses in the following are monic!}\ppnote{I am not even sure if we need this proposition!}
+	\begin{enumerate}
+		\item \emph{Reflexivity:} There is a morphism $(\id_{FY},i,\id_{FY})\c (FY \stackrel{d}{\leftarrow} \Delta_{FY} \stackrel{d}{\to}FY)\to (FY \stackrel{q_1}{\leftarrow} R_Y \stackrel{q_2}{\to}FY)$ in $\spa(\BC)$.
+		\item \emph{Antisymmetry:} Given that $(R_Y \stackrel{s_1}{\leftarrow} A \stackrel{s_2}{\to}R_Y)$ is the pullback along $\brks{q_1,q_2}$ and $\brks{q_2,q_1}$, then there is a morphism $(\id_R,i',\id_R)\c (R_Y \stackrel{s_1}{\leftarrow} A \stackrel{s_2}{\to}R_Y)\to (R_Y \stackrel{d'}{\leftarrow} \Delta_R \stackrel{d'}{\to}R_Y)$ in $\spa(\BC)$.
+		\item \emph{Transitivity:} Given that $(R_Y \stackrel{t_1}{\leftarrow} R_Y\comp R_Y \stackrel{t_2}{\to}R_Y)$ is the pullback along $q_1$ and $q_2$, then there is a morphism $(\id_R,i'',\id_R)\c (R_Y \stackrel{t_1}{\leftarrow} R_Y\comp R_Y \stackrel{t_2}{\to}R_Y)\to (R_Y \stackrel{d'}{\leftarrow} \Delta_R \stackrel{d'}{\to}R_Y)$ in $\spa(\BC)$.
+	\end{enumerate} 
+\end{prop}
+%
+
+\section{Simulations and Bisimulations in Double Categories}
+% Given that $(R \stackrel{s_1}{\leftarrow} P \stackrel{s_2}{\to}R)$ is the pullback along $\brks{p_1,p_2}$ and $\brks{p_2,p_1}$, then there is a morphism $(\id_R,i',\id_R)\c (R \stackrel{s_1}{\leftarrow} P \stackrel{s_2}{\to}R)\to (R \stackrel{d'_1}{\leftarrow} \Delta_R \stackrel{d'_2}{\to}R)$ in $\spa(\BC)$.
 %
 %
 \begin{definition}[Double Relator]\label{def:doub-rela}