On Thu, Mar 6, 2008 at 10:01 AM, Paul B Levy <P.B.Levy@cs.bham.ac.uk> wrote:
Maybe not the walls of mathematics, but what about theorems like "every polynomial functor on Set has a unique initial algebra whose structure map is an identity"? I think theorems like this are worth retaining (and antifoundation makes even more of them).
I'm not familiar with that particular result, but I know other categorical proofs which use set-theoretic ideas like transfinite induction, and so cannot be detached from ZF in an obvious way. On the other hand, there is nothing intrinsically "membership-based" in transfinite induction. The problem seems to be the lack of a categorical analogue of ZF's axiom of replacement, since the sets in V_{\omega+\omega} already form a well-pointed elementary topos with a NNO. I find this especially mysterious because on the surface, replacement merely replaces a set by an isomorphic one (or at most a quotient)! One categorical analogue of replacement comes from categories of classes in algebraic set theory. That is, we move from a categorical analogue of ZF to an analogue of Godel-Bernays set theory. But it seems natural to wonder whether there could be a categorical analogue of replacement expressible solely as a property of the category Set, without reference to how it sits in a category of classes. Has anyone studied this question? Mike