diff --git a/draft/draft.tex b/draft/draft.tex index 6f71ba2..33823d9 100644 --- a/draft/draft.tex +++ b/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}