pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

uncommited from previous time

Browse Source
This commit is contained in:
Sergey Goncharov
2026-09-28 17:03:12 +01:00
parent 1c04675e0a
commit 562aecc62f
1 changed files with 7 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+7 -5
View File
@@ -311,7 +311,7 @@
}% }%
}% }%
} }
\newcommand{\sub}{\mathcal{S}} \newcommand{\sub}{\mathcal{D}_{\leq1}}
\newcommand{\bba}{ \newcommand{\bba}{
@@ -745,7 +745,8 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
\end{proof} \end{proof}
% %
\begin{prop}\label{prop:rel-rela} \begin{prop}\label{prop:rel-rela}
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 of both categories $\rel$ and $\rel_a$, 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 $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the unique witness $w\c R\to S$. Let $(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)$
be jointly-monic spans. Then 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 $\rel_a$ iff there is a morphism $(g_1,g_2,w)$ of the same type in $\rel$, with the unique witness $w\c R\to S$.
\end{prop} \end{prop}
\begin{proof} \begin{proof}
% $(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have: % $(\Rightarrow):$ We define $w$ as $w=\brks{g_1\comp p_1,g_2\comp p_2}$. We have:
@@ -835,7 +836,7 @@ From now on, we use $\spa_a$ and $\rel_a$ to denote the categories of spans and
\draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-2-2); \draw[-{Latex[length=2mm]}] (m-1-2) to[bend right=10] (m-2-2);
% %
\end{tikzpicture} \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$.} \caption{Summary 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} \label{fig:morph-summery}
\end{figure} \end{figure}
%\begin{notation} %\begin{notation}
@@ -1642,7 +1643,7 @@ We have two more notions for coalgebraic bisimulation in $\Set$, that is to defi
\draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2); \draw[-{Latex[length=2mm]}] (m-3-1) to[bend right=5] (m-2-2);
\end{tikzpicture} \end{tikzpicture}
\caption{Summery of results in this section about notions of simulation in $\Set$.} \caption{Summary of results in this section about notions of simulation in $\Set$.}
\label{fig:sim-summery} \label{fig:sim-summery}
\end{figure} \end{figure}
%\begin{center} %\begin{center}
@@ -1756,7 +1757,8 @@ Traditionally, simulations in $\Set$ are defined using relators. In this section
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 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} \end{proof}
\begin{cor} \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}. 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}
are equivalent.
\end{cor} \end{cor}
% %
\begin{prop}\label{prop:HeJ-HuJ} \begin{prop}\label{prop:HeJ-HuJ}