more

draft/draft.tex

@@ -287,6 +287,15 @@
 \newcommand{\gra}{\mathbf{Gra}}
 \newcommand{\obj}{\mathbf{Obj}}
 
+\newcommand{\simeet}{%
+	\mathbin{%
+		\ooalign{%
+			$\sqcap$\cr
+			\hidewidth\raisebox{0.2ex}{\scalebox{0.44}{$\otimes$}}\hidewidth\cr
+		}%
+	}%
+}
+
 
 \newcommand{\bba}{
 \mathrel{%
@@ -1613,13 +1622,14 @@ Then we have
 	\end{tikzcd}
 \end{equation*}
 We recall that in the above diagram $\sigma_3$ is a bisimulation, and the rest are simulations.
-
-We can also define $\join$ and $\meet$ on morphisms as follows:
+\begin{definition}\label{def:join-meet}
+We define $\join$ and $\meet$ on morphisms as follows:
 \begin{gather*}
 	\forall x_1,x_2\in X,\\
 	\sigma_1 \join \sigma_2 (x_1,x_2)= \sigma_1(x_1,x_2) \cup \sigma_2(x_1,x_2),\\
 	\sigma_1 \meet \sigma_2 (x_1,x_2)= (\mathcal{P}p_1)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_1)^\dagger\comp\sigma_2(x_1,x_2)\times(\mathcal{P}p_2)^\dagger\comp\sigma_1(x_1,x_2) \cap (\mathcal{P}p_2)^\dagger\comp\sigma_2(x_1,x_2).
 \end{gather*}
+\end{definition}
 \begin{lemma}\label{lem:proj-dist-set}
 	For relations $R_1$ and $R_2$ the following equation holds:
 	\begin{gather*}
@@ -1779,7 +1789,7 @@ We can also define $\join$ and $\meet$ on morphisms as follows:
 	We have $\sigma(x_1,x_2)\in(\mathcal{P}R)^\dagger$, as $\alpha(x_1)\subseteq\mathcal{P}p_1(R)$ and $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\mathcal{P}p_2(R)$ are inherited from $\delta$ being a simulation structure.
 	Also, it obviously is a simulation as $(\mathcal{P}p_1)^\dagger\comp\sigma(x_1,x_2)=\alpha(x_1)$ and $(\mathcal{P}p_2)^\dagger\comp\sigma(x_1,x_2)\subseteq\alpha(x_2)$ as $(\mathcal{P}p_2)^\dagger\comp\delta(x_1,x_2)\subseteq\alpha(x_2)$. 
 \end{proof}
-\begin{prop}
+\begin{prop}\label{prop:sym-rel-bisim}
 	Assuming that $R$ is a symmetric relation, and $S\neq\emptyset$ is the set of all simulation structures of the type $R\to (\mathcal{P}R)^\dagger$, then the following morphism is the bisimulation structure:
 	\begin{gather*}
 		(\bigmeet_{\sigma\in S}\sigma)\join(\mathcal{P}s)^\dagger\comp(\bigmeet_{\sigma\in S}\sigma)\comp s
@@ -1798,6 +1808,12 @@ We can also define $\join$ and $\meet$ on morphisms as follows:
 	\end{gather*}
 	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. 
+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*}
 \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: