From 8edd2fd9b38e5360eadb2f13b1b3d7f2c64126a7 Mon Sep 17 00:00:00 2001 From: partowp Date: Tue, 30 Jun 2026 14:29:04 +0100 Subject: [PATCH] blah --- draft/draft.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index 78069c9..f821024 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2171,7 +2171,7 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the \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. \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} 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}