prop

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}