[nano_o]

I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example the paper by L. C. Paulson, "A fixedpoint approach to implementing (co)inductive definitions".

So the point of this anti-foundation axiom probably lies somewhere else.

[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.

[tel]

I don't think that either ZFC or ZFC/AFA dominates the other, just that the AFA bakes a framework for infinite streaming structures into the heart of your mathematics. You immediately lose extensional equality in favor of bisimulation, for instance. The point is more to see what centipede mathematics feels like than to claim greater power or expressiveness.