From states to behavior
A coalgebra for an endofunctor $F$ is a map $c : X \to F(X)$. Its form records the observations and transitions available from each state. A stream coalgebra, for example, has $F(X) = A \times X$.
For deterministic labeled transition systems, a suitable functor makes the transition structure explicit. Bisimulation relates states whose observations match and whose successor states remain related.
A semantic qualification
The relationship between bisimulation and equality in a final coalgebra depends on the functor and the existence of that final coalgebra. These hypotheses are part of the theorem, not incidental implementation details.
We invite manuscripts that state these assumptions and test them against concrete concurrent or stateful systems.
This original editorial primer is not a peer-reviewed manuscript.