[tel]

While I haven't yet read that paper, I wanted to point out a thing I just read in a coinduction tutorial (http://www.cs.ru.nl/~bart/PAPERS/JR.pdf).

Coalgebras are defined as an isomorphism between "sets" X==P(A*X) which allow us to unfold our seed state over non-determistic updates. Such a "set" obviously cannot exist in ZFC directly as it violates set cardinality. It can be a set that satisfies the AFA, though—in fact, that equation I just wrote is sufficient to define it I think and then AFA guarantees uniqueness.