From a3927e720b148ccc9e5333c87a3d276c13c093be Mon Sep 17 00:00:00 2001 From: Sergey Goncharov Date: Thu, 28 May 2026 21:15:47 +0100 Subject: [PATCH] pc sync --- ACV-abstract-2026/sym-sim.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ACV-abstract-2026/sym-sim.tex b/ACV-abstract-2026/sym-sim.tex index 3675c5f..faf3360 100644 --- a/ACV-abstract-2026/sym-sim.tex +++ b/ACV-abstract-2026/sym-sim.tex @@ -360,7 +360,7 @@ Take $R=\{(1,2),(2,1),(1,3),(3,1)\}$, and $X=\{1,2,3\}$, and $ c(x)=X$ for every R\setminus\{(1,2)\} & w=(1,3) \end{cases} \end{gather*} -Then $\sigma$ is a witnesses of simulation but not a bisimulation: $c(p_2(1,3))=c(3)=X\neq\mathcal{P}p_2(\sigma(1,3))=X\setminus\{2\}$. +Then $\sigma$ is a witnesses of simulation on $(X,c)$ but not a bisimulation: $c(\pi_2(1,3))=c(3)=X\neq\mathcal{P}\pi_2(\sigma(1,3))=X\setminus\{2\}$. \end{example} %Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the definition by setting $\BC$ to be a regular category, and changing the span $(FR,Fp_1,Fp_2)$ in~\eqref{eq:diag-lax-sim} with the span $((FR)^\dagger,(Fp_1)^\dagger,(Fp_2)^\dagger)$, where $(FR)^\dagger$ is the image of $\brks{Fp_1,Fp_2}$, and $\brks{(Fp_1)^\dagger,(Fp_2)^\dagger}\c(FR)^\dagger\to FX\times FX$ is monic, so $(FR)^\dagger$ is a relation. By the symmetry of $R$ there exists $s\c R\to R$ that we call \emph{swap}, where $p_1\comp s=p_2$ and $p_2\comp s=p_1$. The necessary and sufficient condition for $\sigma$ to be a witness for $R$ to be a bisimulation is that