diff --git a/draft/draft.tex b/draft/draft.tex index 3e61bb6..1e526a6 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -792,23 +792,51 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and \begin{proof} Trivial by the definitions.\qed \end{proof} +%\begin{figure}[t] +% \centering +% \begin{tabular}{|l|c|c|c|c|} +% \hline +% \quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\ +% \hline +% $\spa$ & & & & \\ +% \hline +% $\rel$ & & & & \\ +% \hline +% $\spa_a$ & \ding{56} & & & \\ +% \hline +% $\rel_a$ & & & & \\ +% \hline +% \end{tabular} +% \caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column is in $\Set$.} +% \label{fig:anonymous_onymous-choice} +%\end{figure} \begin{figure}[t] \centering - \begin{tabular}{|l|c|c|c|c|} - \hline - \quad$\Rightarrow$& $\spa$ & $\rel$ & $\spa_a$ & $\rel_a$ \\ - \hline - $\spa$ & & & & \\ - \hline - $\rel$ & & & & \\ - \hline - $\spa_a$ & \ding{56} & & & \\ - \hline - $\rel_a$ & & & & \\ - \hline - \end{tabular} - \caption{Where the axiom of choice is needed to get a morphism on the top row, when a morphism in the left column is in $\Set$.} - \label{fig:anonymous_onymous-choice} + \begin{tikzpicture}[ + scale=0.6, every node/.style={transform shape} + ] + \matrix (m) [matrix of nodes, + nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, + align=center, font=\scriptsize, inner sep=2pt}, + row sep=6mm, column sep=6mm] + { + $\spa$ & $\spa_a$ \\ + $\rel$ & $\rel_a$ \\ + }; + + % Example arrows (uncomment / edit as needed): + \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-1-2); + \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, above] {AC} (m-1-1); + \draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-2-2); + \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-2-1); + \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-2-1); + \draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-1-1); + \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-1-2); + \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-2-2); +% + \end{tikzpicture} + \caption{Summery of results in this section about when we have a morphism in the source of an arrow then we have a morphism in the target in $\Set$.} + \label{fig:morph-summery} \end{figure} %\begin{notation} % In the literature it is common to see a category that has sets as objects, and binary relations as morphims. Here we denote this category $\rel'$. @@ -1411,7 +1439,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi (2): Follows from~\autoref{prop:rel-rela}. (3): ($\Rightarrow$): Assuming there is a morphism in $\spa_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ in $\rel_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then by the assumption there exists $v$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, and it exactly means that $(\alpha(x),\beta(y))\in(FR)^\dagger$, so $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a Hughes-Jacobs bisimulation.\\ - ($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then there exists $v^\dagger\in(FR)^\dagger$ such that $(Fp_1)^\dagger(v^\dagger)=\alpha(x)$ and $(Fp_2)^\dagger(v^\dagger)=\beta(y)$, and since $(FR)^\dagger$ by definition is the image of $\brks{Fp_1,Fp_2}$, so $(FR)^\dagger\subseteq FX\times FY$ that entails $v^\dagger=(\alpha(x),\beta(y))$. Furthemore, since $(\alpha(x),\beta(y))\in(FR)^\dagger$, there exists $v\in FR$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, so we the morphism that we want to be able to say that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation. + ($\Leftarrow$): Assuming there is a morphism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$ we need to prove that exists a morphism of type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{Fp_1}{\leftarrow} FR \stackrel{Fp_2}{\to}FY)$ in $\spa_a$. Assuming $u\in R$ such that $p_1(u)=x$ and $p_2(u)=y$, then there exists $v^\dagger\in(FR)^\dagger$ such that $(Fp_1)^\dagger(v^\dagger)=\alpha(x)$ and $(Fp_2)^\dagger(v^\dagger)=\beta(y)$, and since $(FR)^\dagger$ by definition is the image of $\brks{Fp_1,Fp_2}$, so $(FR)^\dagger\subseteq FX\times FY$ that entails $v^\dagger=(\alpha(x),\beta(y))$. Furthemore, since $(\alpha(x),\beta(y))\in(FR)^\dagger$, there exists $v\in FR$ such that $Fp_1(v)=\alpha(x)$ and $Fp_2(v)=\beta(y)$, so we have the morphism that we want, to be able to say that $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ is a span-based bisimulation. \qed \end{proof} \begin{cor} @@ -1434,22 +1462,50 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi % \begin{figure}[t] \centering - \begin{tabular}{|l|c|c|c|c|} - \hline - \qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\ - \hline - Aczel-Mendler & & & & \\ - \hline - Hermida-Jacobs & \ding{56} & & & \\ - \hline - Span-based & \ding{56} & & & \\ - \hline - Hughes-Jacobs & \ding{56} & & & \\ - \hline - \end{tabular} - \caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.} - \label{fig:bisim-choice} + \begin{tikzpicture}[ + scale=0.6, every node/.style={transform shape} + ] + \matrix (m) [matrix of nodes, + nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, + align=center, font=\scriptsize, inner sep=2pt}, + row sep=6mm, column sep=6mm] + { + Hughes-Jacobs & Hermida-Jacobs \\ + Span-based & Aczel-Mendler \\ + }; + + % Example arrows (uncomment / edit as needed): + \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-1-2); + \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-1-1); + \draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] node[midway, below] {AC} (m-2-2); + \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-2-1); + \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=10] (m-2-1); + \draw[-{Latex[length=2mm]}] (m-2-1) to[bend right=10] (m-1-1); + \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=10] (m-1-2); + \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] node[midway, left] {AC} (m-2-2); + % + \end{tikzpicture} + \caption{Summery of results in this section about notions of bisimulation in $\Set$.} + \label{fig:bisim-summery} \end{figure} +%\begin{figure}[t] +% \centering +% \begin{tabular}{|l|c|c|c|c|} +% \hline +% \qquad Hughes-Jacobs$\Rightarrow$& Aczel-Mendler & Hermida-Jacobs & Span-based & Hughes-Jacobs \\ +% \hline +% Aczel-Mendler & & & & \\ +% \hline +% Hermida-Jacobs & \ding{56} & & & \\ +% \hline +% Span-based & \ding{56} & & & \\ +% \hline +% Hughes-Jacobs & \ding{56} & & & \\ +% \hline +% \end{tabular} +% \caption{Where the axiom of choice is needed to say one bisimulation based on one notion is also a bisimulation with respect to another notion, in $\Set$.} +% \label{fig:bisim-choice} +%\end{figure} \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] @@ -1556,36 +1612,69 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi % \caption{Comparison of anonymous and onymous settings for relations and spans in $\Set$.} % \label{fig:anonymous_onymous_transposed} %\end{figure} - - -\begin{tikzpicture}[ - scale=0.6, every node/.style={transform shape} -] -\matrix (m) [matrix of nodes, - nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, - align=center, font=\scriptsize, inner sep=2pt}, - row sep=6mm, column sep=6mm] -{ - AM-simulation & left-lax simulation\\ - & bi-lax simulation & mid-lax simulation \\ - HJ-simulation & left-lax simulation\\ -}; - -% Example arrows (uncomment / edit as needed): -\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, above] {AC} (m-1-1); -\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1); -\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above] {liftable} (m-2-3); -\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2); -\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, above] {coliftable} (m-2-3); -\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2); -\draw[-{Latex[length=2mm]}] (m-1-2) to node {liftable $\&$ coliftable} (m-2-2); -\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2); -\draw[-{Latex[length=2mm]}] (m-3-2) to node {liftable $\&$ coliftable} (m-2-2); -\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2); -\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1); -\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2); - -\end{tikzpicture} +\begin{figure}[t] + \centering + \begin{tikzpicture}[ + scale=0.6, every node/.style={transform shape} + ] + \matrix (m) [matrix of nodes, + nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, + align=center, font=\scriptsize, inner sep=2pt}, + row sep=6mm, column sep=6mm] + { + AM-simulation & left-lax simulation\\ + & bi-lax simulation & mid-lax simulation \\ + HJ-simulation & left-lax simulation\\ + }; + + % Example arrows (uncomment / edit as needed): + \draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1); + \draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1); + \draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3); + \draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2); + \draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3); + \draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2); + \draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2); + \draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2); + \draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2); + \draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2); + \draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1); + \draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2); + + \end{tikzpicture} + \caption{Summery of results in this section about notions of simulation in $\Set$.} + \label{fig:sim-summery} +\end{figure} +%\begin{center} +%\begin{tikzpicture}[ +% scale=0.6, every node/.style={transform shape} +%] +%\matrix (m) [matrix of nodes, +% nodes={draw, ellipse, minimum width=2.6cm, minimum height=1cm, +% align=center, font=\scriptsize, inner sep=2pt}, +% row sep=6mm, column sep=6mm] +%{ +% AM-simulation & left-lax simulation\\ +% & bi-lax simulation & mid-lax simulation \\ +% HJ-simulation & left-lax simulation\\ +%}; +% +%% Example arrows (uncomment / edit as needed): +%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=30] node[midway, right=3pt] {AC} (m-1-1); +%\draw[-{Latex[length=2mm]}] (m-1-1) to[bend right=30] (m-3-1); +%\draw[-{Latex[length=2mm]}] (m-1-2) to[bend left=30] node[midway, above=8pt] {liftable} (m-2-3); +%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend right=30] (m-1-2); +%\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] node[midway, below=8pt] {coliftable} (m-2-3); +%\draw[-{Latex[length=2mm]}] (m-2-3) to[bend left=30] (m-3-2); +%\draw[-{Latex[length=2mm]}] (m-1-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2); +%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-1-2); +%\draw[-{Latex[length=2mm]}] (m-3-2) to node[midway, right=5pt] {liftable $\&$ coliftable} (m-2-2); +%\draw[-{Latex[length=2mm]}] (m-2-2) to (m-3-2); +%\draw[-{Latex[length=2mm]}] (m-2-2) to[bend right=5] node[midway, above] {AC} (m-3-1); +%\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2); +% +%\end{tikzpicture} +%\end{center} Traditionally, simulations in $\Set$ are defined using relators. In this section we make a comparison on this concept with the other notions of simulation that we mentioned. %\begin{notation} @@ -1634,13 +1723,42 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section \end{definition} % \begin{example} - Given $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation. + Given a functor $F\c\Set\to\Set$ the best example of a relator is the Barr relator. We have already introduced Barr relator, but we did not note it as a relator. It sends every relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}Y)$. It is a symmetric relator. So, every simulation with this relator is actually a bisimulation. \end{example} % -\begin{example} - Given $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{q_1}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{q_2}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote a bi-lax Barr relator of a functor $F$ with $\tilde{F}$. +\begin{lemma}\label{lem:rel-rep} + Given a functor $F\c\Set\to\Set$, for every object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$, we have $(FR)^\dagger=Fp_2\comp (Fp_1)^\op$. +\end{lemma} +\begin{proof} + Since $(FR)^\dagger$ is the image of $\brks{p_1,p_2}$, we have $(FR)^\dagger\subseteq FX\times FY$. For every $x\in FX$ and $y\in FY$ we have $x\mathrel{(FR)^\dagger}y$ iff there exists a unique $u\in FR$ such that $\brks{Fp_1,Fp_2}(u)=(x,y)$, and the latter holds if and only if $(x,y)=(Fp_1(u),Fp_2(u))$, and it is equivalent with saying that $x\mathrel{(FR)^\dagger}y$.\qed +\end{proof} +% +\begin{example}\label{ex:lax-rels} + Given a functor $F\c\Set\to\Set$ with an order structure $\appr$ on it the relator that sends an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel(\BC)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} \appr\comp(FR)^\dagger\comp\appr \stackrel{(Fp_2)^\dagger}{\to}FY)$ is a relator. We call it \emph{bi-lax Barr Relator}. There are other variations of this: left-lax ($\appr\comp(FR)^\dagger$) and right-lax ($(FR)^\dagger\comp\appr$). We denote a bi-lax Barr relator of a functor $F$ with $\tilde{F}$.\\ + Additionally, followed by~\autoref{lem:rel-rep} we have \emph{mid-lax} relator. This relator sends $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ to $(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} Fp_2\comp\appr\comp (Fp_1)^\op \stackrel{(Fp_2)^\dagger}{\to}FY)$. \end{example} % +\begin{prop} + For an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$ that $p_1$ and $p_2$ are surjective, assuming that a set-functor $F$ has a natural order structure $\appr$, the following propositions hold: + \begin{enumerate} + \item If $\appr$ is liftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad Fp_2\comp(Fp_1)^\op\comp\appr$ + \item If $\appr$ is coliftable, we have $Fp_2\comp\appr\comp(Fp_1)^\op\quad=\quad \appr\comp Fp_2\comp(Fp_1)^\op$ + \item If $\appr$ is both liftable and coliftable, all the following are equal: + \begin{itemize} + \item $Fp_2\comp\appr\comp(Fp_1)^\op\quad$ + \item $Fp_2\comp(Fp_1)^\op\comp\appr$ + \item $\appr\comp Fp_2\comp(Fp_1)^\op$ + \item $\appr\comp Fp_2\comp(Fp_1)^\op\comp\appr$ + \end{itemize} + \end{enumerate} +\end{prop} +\begin{proof} + They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed +\end{proof} +\begin{cor} + Assuming that the order structure $\appr$ on a functor $F\c\Set\to\Set$ is liftable and coliftable, all the notions of simulation given by relators mentioned in~\autoref{ex:lax-rels}. +\end{cor} +% \begin{prop}\label{prop:HeJ-HuJ} Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel$, \begin{enumerate}