The covariant powerset functor has no set-based initial model, but it seems that the class of well-founded extensional trees is an initial model. (A tree is well-founded if every downward chain is finite and extensional if no node has two isomorphic branches.) This is well-known to be a model of set theory, Goedel's standard model, in fact. For each n define the nth truncation function, t |--> t|n by saying that t|0 is a bare root and and if t is derived by attaching {t_i} to a bare root then t|n is the extensional reflection (there is one; the obvious equivalence relation is Church-Rosser) of the tree gotten by attaching {t_i|n-1} to a bare root. Every tree is so derived, from well-foundedness. Now define a metric on the class of trees by saying that d(t,t') is 2 to the negative of the greatest n such that t|n = t'|n. In other words the distance is 2^-n if t|n = t|n, but t|n+1 /= t'|n+1. Then the Cauchy completion of this class obviously looks like NWF trees. Does anyone know enough about Aczel's work to tell me if this is a model of his axioms? BTW, this Cauchy completion is a terminal coalgebra for the functor. And it makes a difference whether you Cauchy complete and then take the extensional trees or do it the other way round. In other words, it is possible for the limit of a sequence of non-extensional trees to be extensional, but such trees are _not_ in the model. The decisive example is the NWF set defined by x = {x,{x}}, which is clearly the same as the one defined by x = {x}. (But I defy you to prove it by starting with the first one; it is immediate if you begin with the second.) Michael 333333333333333333333333333333333333