Dear all, I have been thinking lately about the uses of Replacement in ordinary mathematics, viewed from the lens of ETCS. In particular, I wanted to clear up what one might do to circumvent assuming Replacement (or an equivalent) on top of ETCS, for instance. Key examples of what Replacement allows us to do include forming colimits of 'diagrams' specified by logical formulas (for instance the sequence where the n^th term is the coproduct of the P^k(N) for k < n, together with inclusions). I write 'diagrams' since these are not internal diagrams, as is usual in topos theory, nor diagrams (as far as I can tell) in an expanded vocabulary that allows us to talk of functors D --> Set (please correct me if I'm wrong!). In my naivety, I asked a question on MathOverflow [1] asking what is wrong with the suggestion of having some sort of cocompletion of Set (in an external sense) around that allows careful and guarded use of formal colimits, as encoded by diagrams (or 'diagrams' in the above sense). Discussion there didn't proceed as I imagined, but led me to realise (thanks to Zhen Lin and Francois Dorais) that the distinction between internal and external indexing is what is going on. For instance, with the 'diagram' involving iterated powersets above, one must distinguish between the internal natural numbers and the natural numbers in the metalogic. So my question might now be approached in various ways 1) Asking if there a sensible way to talk about cocompletion (or other such constructions) under 'diagrams'. This is somewhat analogous to talking about proper classes in ZFC, which "do not exist", but are handy stand-ins for first-order formulas -- and in fact one might as well work with the category of classes defined as such, or in the "model" of NBG so arising (conservative over ZFC, a desideratum since we are primarily interested in sets) 2) Asking that internal and external natural numbers coincide - this is analogous to \omega-models in material set theory. Of course, this merely copes with 'diagrams' indexed by N (and possibly countable 'diagrams'). This should be enough for cases of the small object argument that only use \omega-many arrows. Obvious generalisations for other ordinals hold, but I suspect that assuming this works for all ordinals implies Replacement (cf [2]). There are obviously analogues for any fixed class of shape of 'diagram': I'm fairly sure that if the diagram exists corresponding to any 'diagram', then any colimit of that shape exists. Any thoughts, comments, or existing work exploring these issues? Thanks, David =References= [1] http://mathoverflow.net/questions/208711/who-needs-replacement-anyway [2] http://jdh.hamkins.org/transfinite-recursion-as-a-fundamental-principle-in-s... -- Dr David Roberts Visiting Fellow School of Mathematical Sciences University of Adelaide SA 5005 AUSTRALIA "When I consider what people generally want in calculating, I found that it always is a number." -- al-Khwārizmī [For admin and other information see: http://www.mta.ca/~cat-dist/ ]