From f2dd939b8ceb7149d65bd38fb47695b986f7b01d Mon Sep 17 00:00:00 2001 From: partowp Date: Fri, 25 Sep 2026 21:33:47 +0100 Subject: [PATCH 1/4] bluh --- draft/draft.tex | 34 ++++++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 1e526a6..f7f358a 100644 --- a/draft/draft.tex +++ b/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} From 96194207bfc9a11d65cacd2af1eefa9ddc7da8c2 Mon Sep 17 00:00:00 2001 From: partowp Date: Sat, 26 Sep 2026 19:55:09 +0100 Subject: [PATCH 2/4] a scheme for something good --- draft/draft.tex | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index f7f358a..b2621fe 100644 --- a/draft/draft.tex +++ b/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)$. From 0482ae66f59c7bba30a35bbcc7ac789ade23cb30 Mon Sep 17 00:00:00 2001 From: partowp Date: Sun, 27 Sep 2026 18:02:05 +0100 Subject: [PATCH 3/4] lemma --- draft/draft.tex | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index b2621fe..40362d2 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2298,18 +2298,19 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio \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)) + \Hom(X,Y)\iso \Hom(\Hom(A,X),\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: + 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*} - \Hom(X,Y)\iso \Hom(\Hom(1,X)\to\Hom(1,Y)) + GX\iso\Hom(\Hom(\argument,X),G) \end{gather*} -\end{cor} + 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*} +\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)$. From 798ca20433d97297ae30e3a053dadded67ec4026 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 28 Sep 2026 15:08:17 +0100 Subject: [PATCH 4/4] fail --- draft/draft.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 40362d2..957ff7d 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2295,7 +2295,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio \end{gather*} \end{definition} % -\begin{lemma} +\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)) @@ -2309,7 +2309,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio 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*} + \end{gather*}\qed \end{proof} % \begin{prop} @@ -2317,7 +2317,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio \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.} + $(\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}