Dear Paul, I do have reveiled my meta-theory, namely ZFC together with the axiom that every set appears as element of some Grothendieck universe. This is not a question of belief but of convenience. I haven't found anything in category theory which needs expressivity beyond that. You ask what I mean by the validity of the statement \forall n:N \exists i : P(X_n)^{X_{n+1}} Iso(i) Well, it has to be read in the internal language of a topos augmented with some `macros' form the language of dependent types (here X -> N is some map in the topos and the formula specifies that it's the family P(N)_{n \in N}. Of course, one might take the pains of Kripke-Joyaling this internal statement BUT why should one want to do so. You are quite right in emphasizing that specifying such a family is one thing and its existence is another one. For the latter purpose one needs the eaxiom of replacement though possibly not its full strength. That's the motivation for my considerations in my "Universes in Toposes". Postulating a class of display maps SS with a strongly generic family E -> U (i.e. this map is in SS and all maps can be obtained as pullback of it) and some desired closure properties. Now supposing N \in U and U being closed under powerset P(-) its is a most simple exercise to construct a map f : N -> U with f(0) = N and f(n+1) = P(f(n)). We have just exploited that P restricts to a map U -> U. This is known since around 1970 when Martin-Loef introduced universes. Of course, he now would not consider something impredicative as the power set functor P but he would consider X \mapsto X^X as an operation on U. Apparently, quite a few category people are not that fond of universes in this sense. So one may ask the question to which extent one may express recursively defined families without universes. The answer given in Paul's book is to require initial fixpoints of endofunctors on some category of families. In case of the example above it would be an endofunctor on EE/N where EE is the topos under consideration. (See www.mathematik.tu-darmstadt.de/~streicher/itpowtop.pdf (temporary!) for one possible way of putting it.) Such an external handling of recursive family is certainly possible but I find it inconvenient because I want to construct my recursive families inside the internal language. In mathematics you never work externally but always internally, i.e. in one single unspecified formal system like ZFC or strengthenings of it (see above). "External" is a logician's idea who considers formal systems, their models and relations between them. But when doing mathematics it's not a good idea to "go external". Thomas PS I find interesting you comments about glueing and the necessity of replacement. I haven't come across this because on the meta-level I use a very strong system where I have it anyway. You are right that via glueing you get a consistency proof for HAH (higher order arithmetic). But this a priori doesn't require replacemnt since Zermelo set theory is sufficient for this purpose.