bluh

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)$.
@@ -2287,8 +2287,34 @@ 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$, 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{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!}
+	\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}