From cd2bc67fe1966e49536108a32f37ef5b42e3031f Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 7 Sep 2026 00:54:28 +0100 Subject: [PATCH] editted a bit! --- draft/draft.tex | 39 +++++++++++++++++++++++++++------------ 1 file changed, 27 insertions(+), 12 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index 1635e48..43e9c2d 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -752,9 +752,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to show the categories of spans and re %\end{notation} \subsection{Categories of Spans and Relations as Double Categories} -As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an arbitrary category $\BC$ is replaced $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms[really?!]. -\todo{Finish at last. "at last" means after finishing the section for simulation without talking about double categories.} -% +As mentioned in the previous section, there is a way to define morphisms in $\spa$ and $\rel$ that can not be captured if an arbitrary category $\BC$ is replaced with $\Set$. We show that $\spa(\BC)$, $\spa_a$, $\rel(\BC)$, and $\rel_a$ are all double categories to give an abstract notion that does capture all the different notions together. Also, double categories show us a way to have $\spa_a(\BC)$ and $\rel_a(\BC)$, i.e., category of spans and category of relations over an arbitrary category $\BC$ with anonymous morphisms. \begin{definition}[(Weak) Double Categories] Given categories $\BC_0$ and $\BC_1$, a double category $\BC_1\rightrightarrows\BC_0$, consists of \begin{itemize} @@ -773,7 +771,7 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp T(\mathcal{R}\odot \mathcal{S})=T\mathcal{S} \end{gather*} \end{definition} -\begin{example} +\begin{example}\label{ex:spa-double-cat} We show that assuming the category $\BC$ has pullbacks, $\spa(\BC)\rightrightarrows\BC$ is a double category. We define $S$ and $T$ as follows: \begin{gather*} S(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)=X_1\\ @@ -781,7 +779,7 @@ As mentioned in the previous section, there is a way to define morphisms in $\sp T(X_1 \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}X_2)=X_2\\ T(g_1,g_2,w)=g_2\\ \end{gather*} - Furthermore, assuming that for every object $X$ in $\BC$ we show the kernel pair of $\id_X$ with $\Delta_X$, we define $UX=\Delta_X$ and for a morphism $f\c X\to Y$ in $\BC$, $Uf$ is the unique morphism $\Delta_f$ in the diagram below that is obtained by the universal property of pullbacks: + Furthermore, for every object $X$ in $\BC$ we show the kernel pair of $\id_X$ with $\Delta_X$, and we define $UX=\Delta_X$ and for a morphism $f\c X\to Y$ in $\BC$, $Uf$ is the unique morphism $\Delta_f$ in the diagram below that is obtained by the universal property of pullbacks: \begin{equation*} \begin{tikzcd}[ampersand replacement=\&] X \& {\Delta_X} \& X \\ @@ -872,7 +870,7 @@ by the universal property of pullbacks, there exists a morphism $u\c R\odot W\to \arrow["{c_V}"', from=2-2, to=2-3] \end{tikzcd} \end{equation*} -So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \stackrel{c_W}{\to}W)\to(S \stackrel{c_S}{\leftarrow} S\odot V \stackrel{c_V}{\to}V)$. So, we define $(f,g,w)\odot(g,h,v)=(w,v,u)$. To define the natural isomorphisms is a cumbersome task, but it is known in the literature. Additionally, showing that $\rel(\BC)\rightrightarrows\BC$ is also a double category is almost the same. The functors are defined the same, except that the functor $\odot$ takes the image of the pullback over its legs, instead of the pullback itself. +So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \stackrel{c_W}{\to}W)\to(S \stackrel{c_S}{\leftarrow} S\odot V \stackrel{c_V}{\to}V)$. So, we define $(f,g,w)\odot(g,h,v)=(w,v,u)$. To define the natural isomorphisms is a cumbersome task, but it is a known fact in the literature. Additionally, showing that $\rel(\BC)\rightrightarrows\BC$ is also a double category is almost the same. The functors are defined the same, except that the functor $\odot$ takes the image of the pullback over its legs, instead of the pullback itself. % The following diagrams help to see why the defined $\odot$ is a functor. % \begin{equation*} % \begin{tikzcd}[ampersand replacement=\&] @@ -959,8 +957,23 @@ So, $(w,v,u)$ is a morphism of type $(R \stackrel{c_R}{\leftarrow} R\odot W \sta % \end{equation*} \end{example} \begin{example} - \todo{Talk about $\spa_a$ and $\rel_a$.} + We show that assuming the axiom of choice, $\spa_a\rightrightarrows\Set$ is a double category. We define the functors $S$, $T$, and $U$ on objects similar to~\autoref{ex:spa-double-cat}, and on the morphisms we define them as follows: + \begin{gather*} + S(g_1,g_2)=g_1\\ + T(g_1,g_2)=g_2\\ + Uf=(f,f) + \end{gather*} + Similarly, the definition of the functor $\odot$ on objects is the same as~\autoref{ex:spa-double-cat}, and for morphisms + \begin{gather*} + (f,g)\c(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(Y \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Z) + \end{gather*} + and + \begin{gather*} + (g,h)\c(Y \stackrel{t_1}{\leftarrow} W \stackrel{t_2}{\to}Z)\to(Z \stackrel{r_1}{\leftarrow} V \stackrel{r_2}{\to}Q) + \end{gather*} + by the axiom of choice and~\autoref{prop:spa-spaa} there exist $c_1\c R\to S$ and $c_2\c W\to V$ such that $(f,g,c_1)$ and $(g,h,c_2)$ are morphisms of the same type in $\spa$. So, as we did show in~\autoref{ex:spa-double-cat} there exists $u\c R\odot W\to S\odot V$ such that $(c_1,c_2,u)\c (R \stackrel{c_R}{\leftarrow} R\odot W \stackrel{c_W}{\to}W)\to(S \stackrel{c_S}{\leftarrow} S\odot V \stackrel{c_V}{\to}V)$ is a morphism in $\spa$ and it is equal with $(f,g,c_1)\odot(g,h,c_2)$, so here we define $(f,g)\odot(g,h)=(c_1,c_2)$. Using $u$ it is obvious that $(c_1,c_2)$ is a morphism in $\spa_a$. Defining the natural isomorphisms are the same for~\autoref{ex:spa-double-cat}. Again, for $\rel_a$ the definitions are similar, except that to define $\odot$ we need to take the image of the pullback over its legs, similar to the case for $\rel(\BC)$.\todo{It is better to double check your last claims.} \end{example} +% \section{Coalgebraic Bisimulation}%\label{sec:} % %\begin{definition}[Relation Lifting] @@ -1294,9 +1307,6 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi \label{fig:anonymous_onymous} \end{figure} % -\subsection{Bisimulation in Double Categories} -\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".} -% \section{Coalgebraic Simulation} \todo{Give an introduction of the definitions for $\spa(\BC)$ and $\rel(\BC)$ that are AM-simulation and HJ-simulation, then open up the discussion about relators.} \begin{definition}[Aczel-Mendler Simulation] @@ -1418,8 +1428,6 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section The proposition entails that Hermida-Jacobs simulation subsumes simulation relations defined with bi-lax Barr relators. \end{rem} Having lax versions of a symmetric relator, allows us to have simulation relations that are related to bisimulation. Also, we did show in the previous proposition that making the commuting diagram lax, with the relator that is not laxed, we get an equivalent definition under the axiom of choice. But if the relator is not symmetric, it is already giving us a notion of simulation, even though we have not laxed it! -\subsection{Simulations in Double Categories} -\todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!} %We show the category of partially ordered sets with monotone functions between them with $\poset$. %\begin{definition}[A Partial Order 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: @@ -1878,6 +1886,13 @@ 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{Bisimulation in Double Categories} +\todo{Start writing this after the section for double categories in the previous section. You should first introduce your definition, and then give all the definitions as examples of your "double coalgebra".} +\subsection{Simulations in Double Categories} +\todo{Try to define simulation in a given double category. Perhaps you need to order enrichment over the endofunctor on $\BC_0$. Then inspired by~\autoref{prop:HeJ-HuJ} you may be able to prove a general theorem for an arbitrary lifting!} +% +% +% \begin{definition}[Double Relator] Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is an endomap on objects and morphisms of category $\BC_1$, for which the following equations hold: \begin{enumerate}