From 6ff5d92bf289269d77edb9f218eb7dd0c64687d4 Mon Sep 17 00:00:00 2001 From: partowp Date: Thu, 25 Jun 2026 22:22:55 +0100 Subject: [PATCH] minor --- draft/draft.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index 8b180aa..d20ca69 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2141,7 +2141,7 @@ Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the \end{cor} \subsection{Maybe Functor} -We prove that symmetric simulation is a bisimulation for the case that $FX=X+1$. First, we prove it for $\Set$. +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} Assuming that $R$ is a symmetric AM simulation over an $F$-coalgebra $(X,\alpha)$ that $FX=X+1$, then for every $(x_1,x_2)\in R$ either \begin{gather*}