diff --git a/draft/draft.tex b/draft/draft.tex index 2896c35..3e61bb6 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -106,6 +106,7 @@ \usepackage{xspace} \usepackage{bm} \usepackage{pifont} +\usepackage{circuitikz} \input{catprog} @@ -1558,21 +1559,31 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi \begin{tikzpicture}[ - scale=0.5, every node/.style={transform shape} + 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] { - $\appr\cdot-$-Hughes-Jacobs & $\appr\cdot-$-Hermida-Jacobs & $\appr\cdot-$-Span-based & $\appr\cdot-$-Aczel-Mendler \\ - $-\cdot\appr$-Hughes-Jacobs & $-\cdot\appr$-Hermida-Jacobs & $-\cdot\appr$-Span-based & $-\cdot\appr$-Aczel-Mendler \\ - $\appr\cdot-\cdot\appr$-Hughes-Jacobs & $\appr\cdot-\cdot\appr$-Hermida-Jacobs & $\appr\cdot-\cdot\appr$-Span-based & $\appr\cdot-\cdot\appr$-Aczel-Mendler \\ + 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-3-2); -\draw[-{Latex[length=2mm]}] (m-3-2) to[bend right=30] (m-3-1); +\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} @@ -1646,6 +1657,28 @@ Given $F\c\Set\to\Set$ and an object $(X \stackrel{p_1}{\leftarrow} R \stackrel{ 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! +%\begin{equation} +% \begin{figure}[!ht] +% \centering +% \resizebox{1\textwidth}{!}{% +% \begin{circuitikz} +% \tikzstyle{every node}=[font=\fontsize{14.2pt}{18.5pt}\selectfont] +% \draw (3,12.5) ellipse (2.125cm and 0.625cm); +% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (3,12.5) {AM-simulation}; +% \draw (8.625,13.125) ellipse (2.25cm and 0.625cm); +% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (8.625,13.125) {HJ-simulation}; +% \draw (1.5,10.375) ellipse (1.875cm and 0.625cm); +% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (1.5,10.375) {F-simulation}; +% \draw (6.75,10.625) ellipse (2.75cm and 0.625cm); +% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (6.75,10.625) {F\comp\appr-simulation}; +% \draw (9.625,8) ellipse (2.625cm and 0.625cm); +% \node [font=\fontsize{14.2pt}{18.5pt}\selectfont, inner xsep=0.080cm, inner ysep=0.085cm, rounded corners=0.020cm] at (9.5,8) {\appr\comp F-simulation}; +% \end{circuitikz} +% }% +% \caption{Your Caption} +% \label{fig:my_label} +% \end{figure} +%\end{equation} %\begin{figure}[t] % \centering % \begin{tabular}{|l|c|c|}