From f7fa996645b848ee66fc6bdb18cdce7454d0247e Mon Sep 17 00:00:00 2001 From: partowp Date: Sun, 14 Jun 2026 19:23:23 +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 c9d72b2..529ef37 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1915,7 +1915,7 @@ We define $\join$ on each $\Hom(X,\powf Y)$ for every sets $X$ and $Y$: %\begin{rem} % Assuming that $\sigma_1$ and $\sigma_2$ are witnesses that $R$ is an Aczel-Mendler simulation from a coalgebra $(X,\alpha)$ to another coalgebra $(Y,\beta)$, then $\sigma_1\meet\sigma_2$ is not necessarily a witness that $R$ is an Aczel-Mendler simulation. %\end{rem} -Since $\subseteq$ is a liftable order, we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut. +Since $\subseteq$ is a liftable order (\autoref{def:liftable-ord}), we have the following lemma. The liftability is not used in the proof, but if $\subseteq$ was not liftable, perhaps we could not prove this. An abstract version of the following lemma is given by Dubut. \begin{lemma}\label{lem:alph-prod} Assuming that $R$ is a relation, and $\sigma\c R\to\powf R$ is a witness for $R$ to be an AM simulation, then exists $\sigma'\c R\to\powf R$ that is another witness for $R$ to be an AM simulation, where $\powf p_1\comp\sigma'=\alpha\comp p_1$. \end{lemma}