diff --git a/draft/draft.tex b/draft/draft.tex index 42cc597..ad269ec 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -1021,7 +1021,7 @@ The given definition is highly abstract. There is a relation lifting that abstra \end{cor} % \subsection{Coalgebraic Bisimulation in Set} -We have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$, respectively called \emph{span-based bisimulation} and \emph{relator-based bisimulation}. +We have two more notions for coalgebraic bisimulation in $\Set$, that is to define them in $\spa_a$ and $\rel_a$, respectively called \emph{span-based bisimulation} and \emph{Hughes-Jacobs bisimulation}. % \begin{definition}[Hughes-Jacobs Bisimulation] A relation $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)$ in $\rel_a$ is a \emph{Hughes-Jacobs bisimulation} over $F$-coalgebras $(X,\alpha)$ and $(Y,\beta)$, whenever there exists a morhpism in $\rel_a$ of the type $(X \stackrel{p_1}{\leftarrow} R \stackrel{p_2}{\to}Y)\to(FX \stackrel{(Fp_1)^\dagger}{\leftarrow} (FR)^\dagger \stackrel{(Fp_2)^\dagger}{\to}FY)$.