how Bisimulations correspond to internal equality on the final coalgebra? From the paper "Towards a mathematical operational semantics" by Turi & Plotkin LICS (1997), in Definition 4.1,  I read :
The greatest $B$-bisimulation $\sim$ is the terminal span over two $B$-coalgebras.
Right after the $\textit{internal equality}$ of a $B$-coalgebra $(X,\alpha)$ is defined as the kernel pair over the identity $id_X$ on the carrier $X$. I am assuming that means the pullback $X \times_X X$ over $X$ along the identity $id_X$.
In Set, when bisimilarity is defined over the terminal $B$-coalgebra, say streams over labels $L$ ($L^\omega$), this coincides with equality (over streams). This is an easy proof.
However, for a generic endofunctor $B$ and from the categorical definitions of bisimilarity and equality I cannot seem to be able to prove it. The paper does not seem to introduce any useful assumption at this point. Any suggestions?
 A: It sounds like the thing you're trying to prove is this: If $X$ is a terminal $B$-coalgebra, then the greatest $B$-bisimulation on $X$ is the internal equality.
First of all, the definition of internal equality as the kernel pair of $\text{id}_X$ is a bit silly. The following square is a pullback:
$$\require{AMScd}
\begin{CD}
X @>\text{id}_X>>  X\\
 @V\text{id}_X VV  @VV\text{id}_XV\\
X @>>\text{id}_X> X
\end{CD}$$
So the kernel pair of $\text{id}_X$ is just the pair of maps $\text{id}_X, \text{id}_X\colon X\to X$. And once you realize this, the rest is rather trivial.
We'd like to show that $(X,\text{id}_X,\text{id}_X)$ is the greatest $B$-bisimulation on $X$, i.e., the terminal span over $X$ and $X$ in the category of $B$-coalgebras.
So suppose we're given a span $(Y,f,g)$ over $X$ and $X$. This is a $B$-coalgebra $Y$, given with two coalgebra morphisms $f\colon Y\to X$ and $g\colon Y\to X$. Since $X$ is the teminal coalgebra, $f = g = {!}$ is the unique coalgebra morphism $Y\to X$. And there is a unique coalgebra morphism ${!}\colon Y\to X$ such that $\text{id}_X\circ {!} = {!}$ and $\text{id}_X\circ {!} = {!}$. We've shown there is a unique morphism of spans from $(Y,f,g)$ to $(X,\text{id}_X,\text{id}_X)$, as desired.
