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

blah

Browse Source
This commit is contained in:
partowp
2026-06-30 14:29:04 +01:00
parent 270f802d80
commit 8edd2fd9b3
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+1 -1
View File
@@ -2171,7 +2171,7 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the
\begin{cor} \begin{cor}
Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well. Considering~\autoref{lem:alph-prod}, assuming that $R$ is a symmetric relation and it is an AM simulation, then $R$ is an AM bisimulation as well.
\end{cor} \end{cor}
Now, we make the proof more abstract. We prove the statement for set-functors of the form $\powf F$, where $F$ is an arbitrary set-functor, and $\powf$ is the powerset functor.
\subsection{Maybe Functor} \subsection{Maybe Functor}
We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$. We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. The order structure that we can define for this functor is that for a set $X$, the order is $\id_X\cup\{(\bot,x)\mid x\in X\}$.
\begin{lemma}\label{lem:maybe-func-set} \begin{lemma}\label{lem:maybe-func-set}