lem

draft/draft.tex

@@ -1809,11 +1809,14 @@ We define $\join$ and $\meet$ on morphisms as follows:
 	By~\autoref{lem:alph-prod} there exists a simulation $\delta\in S$ for which we have $(\mathcal{P}p_1)^\dagger\comp\delta(x_1,x_2)=\alpha(x_1)$. So, $(\mathcal{P}p_1)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)(x_1,x_2)=\alpha(x_1)$. Then by the equations in~\eqref{eq:diag-sym-rel} we also get $(\mathcal{P}p_2)^\dagger\comp((\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s)(x_1,x_2)=\alpha(x_2)$.\qed
 \end{proof}
 \section{Symmetric Simulation in Quantaloids}
-We generalize~\autoref{prop:sym-rel-bisim} in quantaloids. A quantaloid is a category enriched with suplattices. 
+We generalize~\autoref{prop:sym-rel-bisim} in regular quantaloids. A quantaloid is a category enriched with suplattices. 
 Abstractly, first we define an operation that we need on morphisms that takes two simulation witnesses of type $R\to(FR)^\dagger$ to a morphism of type $R\to FX\times FX$:
 \begin{gather*}
 	\sigma_1\simeet\sigma_2=(Fp_1)^\dagger\comp\sigma_1\meet(Fp_1)^\dagger\comp\sigma_2\times(Fp_2)^\dagger\comp\sigma_1\meet(Fp_2)^\dagger\comp\sigma_2
 \end{gather*}
+\begin{lemma}\label{lem:alph-prod-abs}
+	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation witnesses of the type $R\to (FR)^\dagger$, then there exists a simulation witness $\sigma\in S$ that,  $(Fp_1)^\dagger\comp\sigma=\alpha\comp p_1$. 
+\end{lemma}
 \section{Relators}
 We start the discussion with answering the question that why there can be multiple simulation structures based on~\autoref{def:sim}.
 At the moment we have limited the discussion to the category of sets and we are talking about the powerset functor. We know that $\sigma$ is unique in the following diagram: