diff --git a/draft/draft.tex b/draft/draft.tex index 08b029b..3d96d96 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -752,8 +752,212 @@ 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 abstract category $\BC$ is replacing $\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?!]. +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.} +% +\begin{definition}[(Weak) Double Categories] + Given categories $\BC_0$ and $\BC_1$, a double category $\BC_1\rightrightarrows\BC_0$, consists of + \begin{itemize} + \item a category $\BC_0$ of objects and morphisms, + \item a category $\BC_1$ of promorphisms and cells, equipped with a source and target functor $(S\c\BC_1\to\BC_0,T\c\BC_1\to\BC_0)$, a unit functor $U\c\BC_0\to\BC_1$, + \item a category $\BC_2$ of composable promorphisms given by the pullback of $S$ and $T$, and a functor $\odot\c\BC_2\to\BC_1$, and isomorphisms imposing that $\odot$ is associative and unital up to isomorphism. + \end{itemize} + Additionally, the functors have the following properties: + \begin{gather*} + S\comp U=\Id\\ + T\comp U=\Id + \end{gather*} + For $\mathcal{R}$, $\mathcal{S}$ in $\obj(\BC_1)$, if $(\mathcal{R}, \mathcal{S})$ exists in $\obj(\BC_2)$, then: + \begin{gather*} + S(\mathcal{R}\odot \mathcal{S})=S\mathcal{R}\\ + T(\mathcal{R}\odot \mathcal{S})=T\mathcal{S} + \end{gather*} +\end{definition} +\begin{example} + 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\\ + S(g_1,g_2,w)=g_1\\\\ + 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: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + X \& {\Delta_X} \& X \\ + Y \& {\Delta_Y} \& Y \\ + \& Y + \arrow["f"', from=1-1, to=2-1] + \arrow[from=1-2, to=1-1] + \arrow[from=1-2, to=1-3] + \arrow["{\Delta_f}", dashed, from=1-2, to=2-2] + \arrow["f", from=1-3, to=2-3] + \arrow["{\id_Y}"', from=2-1, to=3-2] + \arrow[from=2-2, to=2-1] + \arrow[from=2-2, to=2-3] + \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=2-2, to=3-2] + \arrow["{\id_Y}", from=2-3, to=3-2] + \end{tikzcd} + \end{equation*} + Now, we define $\odot$. For objects $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ and $(Y \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Z)$ in $\spa(\BC)$, we define + \begin{gather*} + (X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\odot(Y \stackrel{q_1}{\leftarrow} S \stackrel{q_2}{\to}Z)=(X \stackrel{p_1\comp c_R}{\leftarrow} R\odot S \stackrel{q_2\comp c_S}{\to}Z), + \end{gather*} + such that $R\odot S$, $c_R$ and $c_S$ are defined in the following pullback in $\BC$: + \begin{gather*} + \begin{tikzcd}[ampersand replacement=\&] + {R\odot S} \& S \\ + R \& Y + \arrow["{c_S}", from=1-1, to=1-2] + \arrow["{c_R}"', from=1-1, to=2-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] + \arrow["{q_1}", from=1-2, to=2-2] + \arrow["{p_2}"', from=2-1, to=2-2] + \end{tikzcd} + \end{gather*} +\end{example} + For morphisms + \begin{gather*} + (f,g,w)\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,v)\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*} + we have the following commutative diagram: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + \&\& {R\odot W} \&\& \\ + X \& R \& Y \& W \& P \\ + Y \& S \& Z \& V \& Q \\ + \&\& {S\odot V} + \arrow["{c_R}"', from=1-3, to=2-2] + \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3] + \arrow["{c_W}", from=1-3, to=2-4] + \arrow["f"', from=2-1, to=3-1] + \arrow["{p_1}"', from=2-2, to=2-1] + \arrow["{p_2}", from=2-2, to=2-3] + \arrow["w", from=2-2, to=3-2] + \arrow["g", from=2-3, to=3-3] + \arrow["{t_1}"', from=2-4, to=2-3] + \arrow["{t_2}", from=2-4, to=2-5] + \arrow["v", from=2-4, to=3-4] + \arrow["h", from=2-5, to=3-5] + \arrow["{q_1}", from=3-2, to=3-1] + \arrow["{q_2}"', from=3-2, to=3-3] + \arrow["{r_1}", from=3-4, to=3-3] + \arrow["{r_2}"', from=3-4, to=3-5] + \arrow["{c_S}", from=4-3, to=3-2] + \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3] + \arrow["{c_V}"', from=4-3, to=3-4] + \end{tikzcd} + \end{equation*} + Since we have + \begin{align*} + r_1\comp v\comp c_W&\\ + &=g\comp t_1\comp c_w\\ + &=g\comp p_2\comp c_R\\ + &=q_2\comp w\comp c_R + \end{align*} + by the universal property of pullbacks, there exists a morphism $u\c R\odot W\to S\odot V$, such that the following diagram commutes: + \begin{equation*} + \begin{tikzcd}[ampersand replacement=\&] + R \& {R\odot W} \& W \\ + S \& {S\odot V} \& V + \arrow["w", from=1-1, to=2-1] + \arrow["{c_R}"', from=1-2, to=1-1] + \arrow["{c_W}", from=1-2, to=1-3] + \arrow["u"', dashed, from=1-2, to=2-2] + \arrow["v", from=1-3, to=2-3] + \arrow["{c_S}", from=2-2, to=2-1] + \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. +% The following diagrams help to see why the defined $\odot$ is a functor. +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% \&\& {R\odot W} \&\& \\ +% X \& R \& Y \& W \& P \\ +% Y \& S \& Z \& V \& Q \\ +% {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ +% \&\& {S'\odot V'} +% \arrow[from=1-3, to=2-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3] +% \arrow[from=1-3, to=2-4] +% \arrow["f"', from=2-1, to=3-1] +% \arrow["{p_1}"', from=2-2, to=2-1] +% \arrow["{p_2}", from=2-2, to=2-3] +% \arrow["w", from=2-2, to=3-2] +% \arrow["g", from=2-3, to=3-3] +% \arrow["{t_1}"', from=2-4, to=2-3] +% \arrow["{t_2}", from=2-4, to=2-5] +% \arrow["v", from=2-4, to=3-4] +% \arrow["h", from=2-5, to=3-5] +% \arrow["{f'}"', from=3-1, to=4-1] +% \arrow["{q_1}", from=3-2, to=3-1] +% \arrow["{q_2}"', from=3-2, to=3-3] +% \arrow["{w'}", from=3-2, to=4-2] +% \arrow["{g'}", from=3-3, to=4-3] +% \arrow["{r_1}", from=3-4, to=3-3] +% \arrow["{r_2}"', from=3-4, to=3-5] +% \arrow["{v'}", from=3-4, to=4-4] +% \arrow["{h'}", from=3-5, to=4-5] +% \arrow["{q_1'}", from=4-2, to=4-1] +% \arrow["{q_2'}"', from=4-2, to=4-3] +% \arrow["{r_1'}", from=4-4, to=4-3] +% \arrow["{r_2'}"', from=4-4, to=4-5] +% \arrow[from=5-3, to=4-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=5-3, to=4-3] +% \arrow[from=5-3, to=4-4] +% \end{tikzcd} +% \end{equation*} +% \begin{equation*} +% \begin{tikzcd}[ampersand replacement=\&] +% \&\& {R\odot W} \&\&\&\&\& {S\odot V} \&\& \\ +% X \& R \& Y \& W \& P \& Y \& S \& Z \& V \& Q \\ +% Y \& S \& Z \& V \& Q \& {Y'} \& {S'} \& {Z'} \& {V'} \& {Q'} \\ +% \&\& {S\odot V} \&\&\&\&\& {S'\odot V'} +% \arrow["{c_R}"', from=1-3, to=2-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=2-3] +% \arrow["{c_W}", from=1-3, to=2-4] +% \arrow["{c_S}"', from=1-8, to=2-7] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-8, to=2-8] +% \arrow["{c_V}", from=1-8, to=2-9] +% \arrow["f"', from=2-1, to=3-1] +% \arrow["{p_1}"', from=2-2, to=2-1] +% \arrow["{p_2}", from=2-2, to=2-3] +% \arrow["w", from=2-2, to=3-2] +% \arrow["g", from=2-3, to=3-3] +% \arrow["{t_1}"', from=2-4, to=2-3] +% \arrow["{t_2}", from=2-4, to=2-5] +% \arrow["v", from=2-4, to=3-4] +% \arrow["h", from=2-5, to=3-5] +% \arrow["{f'}"', from=2-6, to=3-6] +% \arrow["{q_1}"', from=2-7, to=2-6] +% \arrow["{q_2}", from=2-7, to=2-8] +% \arrow["{w'}", from=2-7, to=3-7] +% \arrow["{g'}", from=2-8, to=3-8] +% \arrow["{r_1}"', from=2-9, to=2-8] +% \arrow["{r_2}", from=2-9, to=2-10] +% \arrow["{v'}", from=2-9, to=3-9] +% \arrow["{h'}", from=2-10, to=3-10] +% \arrow["{q_1}", from=3-2, to=3-1] +% \arrow["{q_2}"', from=3-2, to=3-3] +% \arrow["{r_1}", from=3-4, to=3-3] +% \arrow["{r_2}"', from=3-4, to=3-5] +% \arrow["{q'_1}", from=3-7, to=3-6] +% \arrow["{q_2'}"', from=3-7, to=3-8] +% \arrow["{r'_1}", from=3-9, to=3-8] +% \arrow["{r'_2}"', from=3-9, to=3-10] +% \arrow["{c_S}", from=4-3, to=3-2] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-3, to=3-3] +% \arrow["{c_V}"', from=4-3, to=3-4] +% \arrow["{c_{S'}}", from=4-8, to=3-7] +% \arrow["\lrcorner"{anchor=center, pos=0.125, rotate=135}, draw=none, from=4-8, to=3-8] +% \arrow["{c_{V'}}"', from=4-8, to=3-9] +% \end{tikzcd} +% \end{equation*} \section{Coalgebraic Bisimulation}%\label{sec:} % %\begin{definition}[Relation Lifting] @@ -1672,7 +1876,7 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio %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} \begin{definition}[Double Relator] - Given a double category $\BC_1\rightrightarrows\BC_0$, for an endofunctor $F$, an $F$-double relator $\relar$ is a map on the objects of $\BC_1$, for which the following equations hold: + 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} \item $S\comp F=\relar\comp S$ \item $T\comp F=\relar\comp T$ @@ -1680,6 +1884,9 @@ Having lax versions of a symmetric relator, allows us to have simulation relatio \end{enumerate} Additionally, it takes every cell of type $\mathcal{R}\Rightarrow\mathcal{S}$ to a cell of type $\relar\mathcal{R}\Rightarrow\relar\mathcal{S}$. \end{definition} +\begin{remark} + In the above definition we are describing an endomap on objects and morphisms of a category, and we form equations with compositions of this map. The composition that we mean, is the one over functions and not the functors. Indeed, it does not make a functor, but it makes another function. Additionally, the endomap that we define is actually two endomaps on objects and morphism, respectively, but we use the tradition in denoting functors for it that is to use one letter to refer to both maps. Basically, one can think of a relator $\relar$ as a functor that does not preserve identities and compositions. +\end{remark} % \begin{definition}[Double Coalgebra] Given a double category $\BC_1\rightrightarrows\BC_0$, and a $F$-double relator $\relar$, a pair $(\mathcal{R},\delta)$ is an $\relar$-double coalgebra on $\BC_1\rightrightarrows\BC_0$.