Over breakfast neel and I worked out a little diagrammatic version of "what the heck is 'the coinduction principle'", a question that I feel like no matter how many times I answer it for myself, it never stays answered.

The diagram is a cube, two of whose layers look like:

S --> B FS --> FB | | | | v v v v A --> N FA --> FN

And there are arrows from X to FX for every X. The idea is that A and B are two types that we want to try to set up a bisimulation on. F is a functor that we assume has a final coalgebra (N,FN) --- imagine the int-stream functor FX = X × int for a concrete example if you like. Initial algebras have an induction principle which has to do with things belonging to subsets --- which smells equalizerish --- so final coalgebras deserve a coinduction principle that seems coequalizerish, so maybe it should have to do with equating things? Not clear if this last intuition actually makes sense.

Anyway, if we provide the maps from S out to A and B in such a way as to make (S, B, FS, FB) and (S, A, FS, FA) faces of the cube commute, what we have is a bisimulation relation. The relation itself is the span (A, S, B), and the commutativity facts establish that it's a

*bisimulation*; S is the type of "names" for pairs of elements ("states") of A and B, and the map from S to FS gives evidence that for each related pair-state, there is a "next pair state" that can be coherently decomposed into a "next state" for both A and B.

Now (N, FN) is the final coalgebra, so we get unique arrows from S, B, and A all into N such that the appropriate faces of the cube commute. But if we do a bit of a diagram chase, we see that the (S, A, N) path and the (S, B, N) path both satisfy the property that uniquely characterizes the (S, N) arrow; so they're all equal, and the (S, A, B, N) square commutes.

But that's exactly what we want to know! I'll describe it in terms of the int stream: the arrows from A and B to N are unfolds of the stream-generators that are the arrows A to FA and B to FA. If we choose an arbitrary element of S, we've chosen an arbitrary

*related*pair of elements, one each from A and B, and the commutativity of the square says that their unfolded streams are equal!