minor

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 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\}$.
+Then $\sigma$ is a witnesses of simulation on $(X,c)$ but not a bisimulation: $c(p_2(1,3))=c(3)=X\neq\mathcal{P}p_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