From 89aeaf7461fd20b9d916c8a5b60b67800d16188c Mon Sep 17 00:00:00 2001
From: partowp <partowp@UOB25BXTXG74.adf.bham.ac.uk>
Date: Tue, 28 Jul 2026 12:22:02 +0100
Subject: [PATCH] the prop

---
 draft/draft.tex | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/draft/draft.tex b/draft/draft.tex
index 8dee0bc..6540bab 100644
--- a/draft/draft.tex
+++ b/draft/draft.tex
@@ -3337,8 +3337,19 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat
 \end{proof}
 \todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!}
 \begin{prop}
-Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is a $\hat{\relar}$-bisimulation.
+Assuming that $r$ is a symmetric relation, and it is an $\relar$-simulation on a coalgebra $(X,\alpha)$, then $r$ is an $\hat{\relar}$-bisimulation.
 \end{prop}
+\begin{proof}
+	$r$ being an $\relar$-simulation means that $r\leq \alpha^\op\comp\relar r\comp\alpha$, and $r$ being symmetric means that $r^\op=r$. So, we need to prove that $r\leq\alpha^\op\comp\hat{\relar} r\comp\alpha$. We have:
+	\begin{align*}
+		x \mathrel{(\alpha^\op\comp\hat{\relar} r\comp\alpha)} y&\\
+		\iff &x\mathrel{(\alpha^\op\comp(\relar r\cap (\relar r)^\op)\comp\alpha)} y\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{(\relar r\cap (\relar r)^\op)}y'\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad x'\mathrel{(\relar r)^\op}y'\\
+		\iff &\exists x',y',\quad x\mathrel{\alpha}x'\quad\&\quad y\mathrel{\alpha}y'\quad\&\quad x'\mathrel{\relar r}y'\quad\&\quad y'\mathrel{\relar r}x'
+	\end{align*}
+	Now, assuming $x\mathrel{r}y$ gives us $x\mathrel{(\alpha^\op\comp\relar r\comp \alpha)} y$ that is equivalent with saying that exist $x'$ and $y'$ such that $x\mathrel{\alpha}x'$, $y\mathrel{\alpha}y'$, and $x'\mathrel{\relar r}y'$. Since $r$ is symmetric, we have $y\mathrel{r} x$ that means that exist $x''$ and $y''$ such that $x\mathrel{\alpha}x''$, $y\mathrel{\alpha}y''$, and $y''\mathrel{\relar r}x''$. On the other hand since $\alpha$ is a function, we have $x''=x'$ and $y''=y'$, so we have $y'\mathrel{\relar r}x'$ that ultimately gives $x\mathrel{(\alpha^\op\comp\hat{\relar}r\comp\alpha)}y$. So, $r$ is an $\hat{\relar}$-bisimulation as well.\qed
+\end{proof}
 \end{document}