The statement has been made in several places that forcing in logic is similar to or the same as sheafification. Also MacLane, Categories for the Working Mathematician, has an appendix entitled "Foundations", with the following statement: "However, categories can be described directly---and they can then be used as a possible foundation for all of mathematics, thus replacing the use in such a foundation of the usual Zermelo-Fraenkel axioms for set theory."
The summary in this appendix is (for me at least) just an informal sketch of the point. When I read this before, it was never clear to me to what extent you really get a full alternative to set-theoretic axioms. (Or to first-order logic? Or to propositional calculus?)
Or to what extent some other category can be addressed by axioms like the category of sets. In fact in standard set theory you do work with the category of ordinals as well as the category of sets. Could there be useful axioms expressed in terms of the category of groups or rings or something like that?
It seems strange that a lot of mathematics involves two orthogonal formalisms thrown together, category theory and set theory. For instance, for me personally the distinction between small and large categories has only be been useful for negative reasons. How much is there to what MacLane promises? (Maybe there is a lot and I just don't know about it.)
Well, there is a book that could help with my head-scratching, Topoi, the categorical analysis of logic, by Robert Goldblatt.
