more wrtiting

draft/draft.tex

@@ -1939,9 +1939,9 @@ To define $\delta$, we define $c\c(\mathcal{P}R^\dagger)\to((\mathcal{P}R^\dagge
 \begin{notation}
 	From now on, we show relations with small letters, and for two relations $r_1$ and $r_2$ by $r_1\leq r_2$ we mean $r_1\subseteq r_2$. Also, we show the category of relations over set that we represent by spans with $\spa$, and $\rel$ is the category of sets and binary relations between them.
 \end{notation}
-\begin{prop}
+\begin{lemma}\label{lem:rel-span-equiv}
 	$r\c X\rto Y$ is a morphism in $\rel$ iff there is an object $(r,p_1,p_2)$ in $\spa$.
-\end{prop}
+\end{lemma}
 \begin{proof}
 	($\Rightarrow$): $r\c X\rto Y$ being a morphism in $\rel$ means that in $\Set$ there exist an object $r$ with a unique mono of type $r\to X\times Y$ that is a pairing that we show with $\brks{p_1,p_2}$. So, $(r,p_1,p_2)$ form an object in $\spa$.
 	
@@ -1952,9 +1952,9 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	Assuming $F$ is a functor on $\Set$, a $F$-relator or simply a relator $\relar$ is a monotone map that sends a morphism of $\Rel$ that is a relation $X\rto Y$ to $FX\rto FY$. 
 \end{definition}
  
-\begin{definition}[Hermida-Jacobs Simulation]
+\begin{definition}[Hermida-Jacobs Simulation]\label{def:hej-sim}
 	For a relator $\relar$ on a functor $F$ a HJ-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ is a relation $r$ for which there exists a morphism $\sigma\c r\to\relar r$ called \emph{witness} such that the following diagram commutes ($;$ is the relation composition):
-	\begin{equation*}\label{def:hej-sim}
+	\begin{equation}\label{eq:hej-sim}
 		\begin{tikzcd}[ampersand replacement=\&]
 			X \& r \& Y \\
 			{FX} \& {\relar r} \& {FY}
@@ -1966,11 +1966,19 @@ The above translation seems to be true in a more general case, where $\spa$ and
 			\arrow["{{(Fp_1)}^\relar}", from=2-2, to=2-1]
 			\arrow["{{(Fp_2)}^\relar}"', from=2-2, to=2-3]
 		\end{tikzcd}
-	\end{equation*}
+	\end{equation}
 \end{definition}
 
 \begin{definition}[Relator-based Simulation]
-	Given a relator $\relar$, a relation $r\c X\rto Y$ is an $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$,	i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
+	Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-simulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r\leq \alpha;\relar r;\beta^\op$,	i.e, if $(x,y)\in r$ entails $(\alpha(x),\beta(y))\in\relar r$, for all $x\in X$ and $y\in Y$.
+\end{definition}
+
+\begin{definition}[Symmetric Relator]
+	A relator $\relar$ is symmetric if and only if for every relation $r$ we have $\relar(r^\op)=(\relar r)^\op$.
+\end{definition}
+
+\begin{definition}[Relator-based Bisimulation]
+	Given a relator $\relar$, a relation $r\c X\rto Y$ is a $\relar$-bisimulation from a coalgebra $\alpha\c X\to FX$ to a coalgebra $\beta\c Y\to FY$ if $r$ is a $\relar$-simulation, and $\relar$ is a symmetric relator.
 \end{definition}
 
 \begin{notation}
@@ -1985,16 +1993,18 @@ The above translation seems to be true in a more general case, where $\spa$ and
 \end{proof}
 
 \begin{prop}
-	A relation $r$ is a $\relar$-simulation if and only if it is a HJ-simulation with the witness $\sigma\c r\to\relar r$.
+	For a relator $\relar$ of a functor $F$, a relation $r$ is a $\relar$-simulation from $\alpha\c X\to FX$ to $\beta\c Y\to FY$ iff it is a HJ-simulation with the witness $\sigma\c r\to\relar r$.
 \end{prop}
 \begin{proof}
-	\todo{Finish}
+	($\Rightarrow$): $r$ being a $\relar$-simulation means that $x\;r\;y$ gives $\alpha(x)\;\relar r\;\beta(y)$. Since $r$ and $\relar r$ are both relations, by~\autoref{lem:rel-span-equiv} there exist objects $(r,p_1,p_2)$ and $(\relar r,(Fp_1)^\relar,(Fp_2)^\relar)$ in $\spa$. We define $\sigma\c r\to\relar r$ to be $\sigma(x,y)=(\alpha(x),\beta(y))$. $\sigma$ commutes in~\eqref{eq:hej-sim}, so we have a HJ-simulation.
+	
+	($\Leftarrow$): Assuming we have a $\sigma$ that commutes in~\eqref{eq:hej-sim}, we want to prove that if $x\;r\;y$ we have $\alpha(x)\;\relar r\;\beta(y)$. By~\eqref{eq:hej-sim} we have $\alpha\comp p_1=(Fp_1)^\relar\comp\sigma$ and $\alpha\comp p_2=(Fp_2)^\relar\comp\sigma$. It means that since $x\;r\;y$ then exists $w\in\relar r$, such that $\sigma(x,y)=w$, where $(Fp_1)^\relar(w)=\alpha(x)$ and $(Fp_2)^\relar(w)=\beta(y)$. So, we have $\alpha(x) \;\relar r \;\beta(y)$.\qed
 \end{proof}
 \begin{prop}
 	For an arbitrary relator $\relar$ on a functor $F$, if a relation $r$ is a HJ-simulation, the witness is unique.
 \end{prop}
 \begin{proof}
-	It only relies on the fact that ${(Fp_1)}^\relar_\appr$ and ${(Fp_2)}^\relar_\appr$ in~\eqref{def:hej-sim} are jointly monic.\qed
+	It only relies on the fact that ${(Fp_1)}^\relar$ and ${(Fp_2)}^\relar$ in~\eqref{def:hej-sim} are jointly monic.\qed
 \end{proof}
 \begin{definition}
 	We call $\hat{\relar}$ a symmetrization of a relator $\relar$ iff for a relation $r$ it is defined as follows:
@@ -2015,6 +2025,43 @@ The above translation seems to be true in a more general case, where $\spa$ and
 \begin{remark}
 	If we want to have the previous corollary for two different coalgebras $\alpha\c X\to FX$ and $\beta\c X\to FX$, we need to assume that $r^\op$ is also a $\relar$-simulation from $\beta$ to $\alpha$. 
 \end{remark}
+\begin{prop}
+	$\hat{\relar}$ is a symmetric relator, i.e., every $\hat{\relar}$-simulation is actually a $\hat{\relar}$-bisimulation.
+\end{prop}
+\begin{proof}
+	\begin{align*}
+		\hat{\relar}(r^\op)&\\
+		&=\relar(r^\op)\cap(\relar (r^\op)^\op)^\op\\
+		&=\relar(r^\op)\cap(\relar r)^\op\\
+		&=(\relar r)^\op\cap\relar(r^\op)\\
+		&=(((\relar r)^\op\cap\relar(r^\op))^\op)^\op\\
+		&=(\relar r\cap(\relar(r^\op))^\op)^\op\\
+		&=(\hat{\relar}r)^\op
+	\end{align*}\qed
+\end{proof}
+\begin{definition}[Behavioural Equivalence]
+	Assuming $F\c\Set\to\Set$, behavioural equivalence from a $F$-coalgebra $(X,\alpha)$ to a $F$-coalgebra $(Y,\beta)$ is a relation $r\subseteq X\times Y$, such that there exists a coalgebra $(Z,\gamma)$ and morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ for every $(x,y)\in r$, $f(x)=g(y)$. 
+\end{definition}
+
+\begin{definition}
+	A relation $r\c X\rto Y$ is difunctional iff there are functions $f\c X\to Z$ and $g\c Y\to Z$ such that for every $(x,y)\in R$ we have $f(x)=g(y)$.
+\end{definition}
+
+\begin{definition}[Soundness and Completeness of Relators]
+	A relator $\relar$ is sound iff the $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is less than or equal to their behavioural equivalence, and it is complete iff it is greater than or equal to their behavioural equivalence.
+\end{definition}
+
+\begin{thm}
+	Let $\relar$ be a relator for a functor $F$:
+	\begin{enumerate}
+		\item If for all functions $f\c X\to A$ and $g\c Y\to A$, $\relar(g^\op\comp f)\geq (Fg)^\op\comp Ff$, then $\relar$-similarity is complete.
+		\item If $\relar$ preserves difunctional relations and for every epi-cospan $(f\c X\to A,g\c Y\to A)\in\Set$, $\relar(g^\op\comp f)\leq(Fg)^\op\comp Ff$, then $\relar$-similarity is sound.
+	\end{enumerate}\qed
+\end{thm}
+
+\begin{prop}
+	$\hat{\relar}$ is sound and complete.
+\end{prop}
 \end{document}