From e9bc1cba676096eafd6dc8c71cd5e8c014fa2f0a Mon Sep 17 00:00:00 2001
From: partowp <partowp@UOB25BXTXG74.adf.bham.ac.uk>
Date: Wed, 29 Apr 2026 00:08:18 +0100
Subject: [PATCH] some statements added

---
 draft/draft.tex | 35 +++++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/draft/draft.tex b/draft/draft.tex
index aa48346..0ad1290 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -1935,6 +1935,9 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 	u(\inr w)=w
 \end{gather*}
 \subsection{Symmetric simulation}
+\begin{notation}
+	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$.
+\end{notation}
 \begin{definition}[Relator]
 	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$. 
 \end{definition}
@@ -1957,8 +1960,26 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 \end{definition}
 
 \begin{definition}[Relator-based Simulation]
-	Given a relator $\relar$, a relation $r\c X\rto Y$ is an $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \beta^\op\comp\relar R\comp \alpha$,	i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
+	Given a relator $\relar$, a relation $r\c X\rto Y$ is an $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$,	i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
 \end{definition}
+
+\begin{notation}
+	From now on we refer to relator-based simulations of a relator $\relar$ with $\relar$-simulation. If we talk about a HJ-simulation we specify the witness.
+\end{notation}
+
+\begin{lemma}\label{lem:sim-simp}
+	$r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. 
+\end{lemma}
+\begin{proof}
+	$r$ being a $\relar$-simulation means $r\leq\beta^\op\comp\relar r\comp\alpha$, meaning that if $x\;r\;y$ then $x \;\alpha;\relar r;\beta^\op\; y$, and it means that there exist $w\in\relar r$ that its first element is equal with $\alpha(x)$ and its second element is equal with $\beta(y)$, enabling us to say $\alpha(x)\;\relar r\; \beta(y)$.\qed
+\end{proof}
+
+\begin{prop}
+	A relation $r$ is a $\relar$-simulation if and only if it is a HJ-simulation with the witness $\sigma\c r\to\relar r$.
+\end{prop}
+\begin{proof}
+	\todo{Finish}
+\end{proof}
 \begin{prop}
 	For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique.
 \end{prop}
@@ -1972,8 +1993,18 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 	\end{gather*}
 \end{definition}
 \begin{prop}
-	Assuming that $\relar$ is a relator, and $r$ is a symmetric relation that is a simulation for $\relar$, then $r$ is also a simulation for $\hat{\relar}$.
+	Assuming that $\relar$ is a relator, and $r$ and $r^\op$ are both $\relar$-simulations from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ and vice-versa respectively, then $r$ is also a $\hat{\relar}$-simulation.
 \end{prop}
+\begin{proof}
+	We need to prove that $x\; r\;y$ gives $\alpha(x)\;\hat{\relar} r\;\beta(y)$.
+	 $r$ being a $\relar$-simulation means that assuming $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. So, we are left to prove $\alpha(x)\;(\relar (r^\op))^\op\;\beta(y)$. $x\;r\;y$ gives $y\;r^\op\;x$, and $r^\op$ being a $\relar$-simulation from $\beta$ to $\alpha$ gives $\beta(y)\;\relar r^\op\; \alpha(x)$. So, we have $\alpha(x) \;(\relar(r^\op))^\op \;\beta(y)$. \qed
+\end{proof}
+\begin{cor}
+	Assuming that $\relar$ is a relator, and $r$ is a symmetric $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to itself, then $r$ is also a $\hat{\relar}$-simulation.
+\end{cor}
+\begin{remark}
+	If we want to have the previous corollary for two different coalgebras $\alpha\c X\to FX$ and $\beta\c X\to FX$, we need to assume that $r^\op$ is also a $\relar$-simulation from $\beta$ to $\alpha$. 
+\end{remark}
 \end{document}