Doing without AFA: final coalgebras in ZF. We mentioned in note [2] that it is possible to alter the pairing operation in such a way that one may prove many of the results that our treatment obtains only by using ZFA.  This points is mentioned in Forster (1994) and developed in detail in Paulson (1999) (and in other papers by Paulson). One replaces the Kuratowski pair ⟨x,y⟩ with a variant, ({0}× a)∪ ({1}× b).  (This is the usual disjoint union operation, also called the coproduct on sets.)  Then one defines variants of other notions: the cartesian product, functions, etc.  And in terms of these one can indeed study streams and infinite trees, and many other sets of interest in this entry.  Even more, one can prove final coalgebra theorems, stating sufficient conditions for the existence of a final coalgebra whose structure is the identity. (This is an important point for this line of work: in ZF we can  show the existence of final coalgebras for the same functors as in ZFA, but in the latter theory we can get final coalgebras whose structure maps are the identity.) 