The set theory ETCS famously comes without the Replacement axiom schema (or an equivalent) that is part of ZFC. One (to me, not apparently useful) set that one cannot build in ETCS is $\coprod_{n\in \mathbb{N}} P^n(\mathbb{N})$. Jacob Lurie pointed out on Michael Harris' blog^{1} the example of taking a Banach space $V$ and considering the colimit of the sequence $V \to V^{**}\to V^{*4} \to \cdots$. Yemon Choi responded to a foolish suggestion of mine that this sequence (or rather, the related cosimplicial object) is in fact of use.

This got me to thinking that from a category-theoretic point of view, we are used to not having enough colimits (say in geometric settings, like schemes, manifolds, and so on) or limits (for instance in settings like finite groups etc), and this is deftly sidestepped by using a colimit completion. One can consider ind-schemes, or differentiable stacks, etc etc. Why should ETCS be any different, apart from intending to be the primordial category?

What stops me from working, when I need to, in a slightly larger category that is in a sense a colimit-completion of an ETCS category, with the understanding that most of the time I'm interested in objects in my original category, but sometimes constructions I'm interested in sit outside it? The original example above is perfectly well represented as the sequence $k\mapsto \coprod_{0\leq n\leq k} P^n(\mathbb{N})$, with the obvious inclusions between them.

Note that I'm not asking that arbitrary objects in the completed category are necessarily the stuff of ordinary mathematics, or that the completed category is a topos, or a model of ETCS. But what can go wrong with this approach? What are the usual uses of Replacement in "ordinary mathematics" (almost anything that's not ZFC-and-friends) that could/couldn't be sorted by the method proposed above?

^{1} The context of the discussion was the effect on ordinary mathematics the discovery that ZFC was inconsistent. Tom Leinster argues (and I agree) that the most likely culprit would be Replacement, since the rest of ZFC is essentially equivalent to ETCS, and the axioms of ETCS encode the operations on sets that underly day-to-day practice of people who aren't set theorists.

[EDIT: On reflection, I'm putting words into Tom's mouth a little here. The actual point he has made is that *if* a contradiction were found with using Replacement, it wouldn't affect most mathematicians, but it a contradiction were found in ETCS (equivalently, BZC) then we could start to worry. If we assume that 'ordinary' mathematics is consistent, as it seems to be, then one might make the---justified or not---leap that a little-used axiom is the place a contradiction might be found, if one existed. As others have pointed out in the comments below, Comprehension is also a contender for a 'risky' axiom.]

alwaysbothers me when people from category theory question Replacement. The idea behind the categorical approach, as I understand it, is that functions are more important than elements. Replacement tells you the universe is closed under definable functions. Functions! $\endgroup$ – Asaf Karagila♦ Jun 8 '15 at 6:09neededfor the proof. So no "hack" is available. $\endgroup$ – Monroe Eskew Jun 8 '15 at 8:1541more comments