minor

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*}