It is, of course, true that Maurer's and AST's form of replacement is stronger than the SCHEMA of replacement because it quantifies over all families in the topos and not just the syntactically definable ones. The same "mistake" appears in the definition of Grothendieck universes. Set theorist insist on formulating set theory in first order logic and therefore must formulate replacement as a schema since they can't quantify over families of sets (the ambient category is a logos or Heyting category but not cartesian closed). If they decided to formulate set theory within higher order logic they presumably would have formulated replacement not as a schema (see Bill's remarks on Goedel and Kreisel's suggestions). But of course there is no problem to adapt Maurer's notion of replacement to the schema form. Nevertheless, since in the schema of replacement there may occur free variables one has to be careful when quantifying over functions representable by formulas in the language of set by considering all reindexings along U^n -> 1. This is not done in McLarty's article. He just gives a reformulation of the replacement schema WITHOUT free variables. I presumably tried to pack too much into my mail and thus (again) forgot about the distiction between schema and the stronger from (sorry Bill!). My intention was to advocate the necessity of an object U of sets which is not available in (models of) ETCS. So one cannot directly interpret the language of set theory in a model of ETCS but has first to CONSTRUCT a model for set theory from it. But this is only possible because models of ETCS are wellpointed. So if one is interested in models of constructive set theory ETCS is not particularly helpful. Thomas