Paul Levy 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 sure what "retaining" means here. Does the category Set, even as a cartesian category, have *any* properties that are open to debate? (Other than by intuitionists, who seem to thrive on quicksand.) For Set as a cartesian closed category I can see room for debate about the number of nonisomorphic sets that can appear along a chain of monics from X to 2^X when X is infinite (defined say as admitting endomonics that are not automorphisms), but relatively little in practical mathematics seems to hinge on the outcome. Correct me if I'm wrong, but my impression is that for any given language in which to express properties of Set, whether that of categories, cartesian categories, cartesian closed categories, or toposes, the properties of Set, understood classically and up to equivalence, are essentially fixed modulo largely irrelevant minutiae such as the above. Your example is a perfectly identifiable property of any category with polynomial functors (suitably defined) such as Set. If the polynomial functors are those generated from the identity functor by binary product and coproduct, e.g. X, X+X, X^2, X+X^2, etc. then it holds of Set because then the initial algebra is always the empty set (but you probably had the empty product 1 in mind as well). If Set didn't have that property it wouldn't be Set, just as Z wouldn't be Z if integer addition wasn't commutative. The property P = "for all objects x and y there exists a set z for which x is a subset of z and y is a member of z" holds of all models of ZF. It cannot be said to hold of the category Set however, not because we can't prove it, i.e. can't imagine how assuming it false could do any harm, but because we can't define it, i.e. can't imagine how it could be either true or false. What does it even mean when applied to Set as a category, or as a cartesian closed category, or even as a topos? More structure than that has to be added to Set to make P meaningful. The same goes for AFA. Chapters 1-6 of Aczel are developed starting within the ZF framework. Categories enter at Chapter 7, but Set is already fully encumbered at that point with all the machinery necessary to interpret all sentences of the language of ZF, where P is true. In that sense even FA (the Foundation Axiom) creates properties of Set that are not meaningful for Set as a mere topos. AFA as a weakening of FA means that generically there are fewer properties than with FA, not more. Fixing a particular model of AFA creates properties specific to the model, which may or may not contradict FA. (Every model of ZF is automatically a model of ZF-FA+AFA.) Vaughan