 To put things differently, and to ask a question that surely belongs in this entry, why should one work with AFA instead of FA?  Much depends on the purposes one brings to set theoretic modeling in the first place.  For most purposes, including most of mathematics, it makes little or no difference.  To model some circular phenomena, it turns out to be convenient to work with final coalgebras of various functors.  It is especially nice with the structure maps on those final coalgebras may be taken to be the identity function.  For example, this would allow us to say that a stream of numbers really and truly is an ordered pair of a number and a stream.  In this case, having AFA would be nice, but the results above show that in many of the interesting cases, it is not actually needed.  On the other hand, if one is content to work with isomorphisms, then having the structure map be the identity is a kind of “optional extra”.  Further, the question of which axiom to adopt might appear to be besides the point.