Paul B Levy wrote in part:

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).

This is so fundamental that I'm inclined to make it an axiom. (Well, we can leave uniquiness --up to isomorphism, you mean-- and the invertibility of the structure map for theorems.) This is essentially an axiom of the Calculus of Inductive Constructions, which (like most modern type theory) is easily put in categorial language.

I'd also like to suggest that "foundations" is being used in two very different senses. In FoM, it's about quantifying the philosophical risks involved in particular formal systems and proofs, i.e. issues such as relative consistency, omega-consistency, etc. For this purpose the primacy of membership vs composition is quite immaterial.

All the same, I find these matters much easier to understand when I think about them in terms of categories of sets, rather than in terms of (models of a) membership-based set theory. I would be able to read FoM if it weren't so hostile to this (although I'll follow Vaughn in noting that I haven't looked lately, so I can't speak for what it's like now).

Category theory on the other hand is about fundamental algebraic structures. I don't think it makes sense to ask "is category theory omega-consistent?" as one can for ZF (not that anyone knows the answer).

No, but one can ask of a topos with a natural-numbers object N (and satisfying other properties that match various axioms of ZF), given a morphism X -> N whose pullbacks 0, 1, 2, ...: 1 -> N are all occupied (so each pullback has a morphism from 1), whether the negation of X over N (the internal hom [0, X] taken in the slice category over N) can also be occupied. --Toby