more

draft/draft.tex

@@ -2040,10 +2040,10 @@ The above translation seems to be true in a more general case, where $\spa$ and
 	\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)$. 
+	Two states $x$ and $y$ of two coalgebras $(X,\alpha)$ and $(Y,\beta)$ are behaviourally equivalent iff there exist a coalgebra $(Z,\gamma)$ and coalgebra morphisms $f\c(X,\alpha)\to(Z,\gamma)$ and $g\c(Y,\beta)\to(Z,\gamma)$ such that $f(x)=g(y)$. The relation $r$ consisting of all behaviourally equivalent states of these two coalgebras is called behavioural equivalence.
 \end{definition}
 
-\begin{definition}
+\begin{definition}[Difunctional Relation]
 	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}