From 1123f4281058992cd5b80f5b4600e1dfdf064328 Mon Sep 17 00:00:00 2001 From: partowp Date: Sat, 25 Jul 2026 17:24:45 +0100 Subject: [PATCH] prop --- draft/draft.tex | 3 +++ 1 file changed, 3 insertions(+) diff --git a/draft/draft.tex b/draft/draft.tex index 7ace02f..8dee0bc 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -3336,6 +3336,9 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \todo{Write it down. You have it in your notes.} \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. +\end{prop} \end{document}