a scheme for something good

draft/draft.tex

@@ -2288,6 +2288,37 @@ 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.
 \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}
+	Given objects $A$, $X$, and $Y$ in a category $\BC$, then we have:
+	\begin{gather*}
+		\Hom(X,Y)\iso \Hom(\Hom(A,X)\to\Hom(A,Y))
+	\end{gather*}
+\end{lemma}
+\begin{proof}
+	It is entailed by the Yoneda lemma. \todo{Finish! You may need cartesian closedness!}
+\end{proof}
+\begin{cor}
+	Given objects $X$ and $Y$ in a category $\BC$, then we have:
+	\begin{gather*}
+		\Hom(X,Y)\iso \Hom(\Hom(1,X)\to\Hom(1,Y))
+	\end{gather*}
+\end{cor}
+%
+\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):$ \todo{Finish, using the concrete proof.}
+\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*}
@@ -2303,8 +2334,19 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio
 	\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}
-	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!}
+	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)$.