This is a question that I have seen asked passively in comments relating to the separation of category theory from set theory, but I haven't seen it addressed in full.


I know that it's possible to formulate category theory within set theory while still being albe to construct the useful things one would want from category theory. So as far as I understand, all normal mathematics that involves category theory can be done as long as a little caution is taken. 


I also know that some people (categorical foundationalsists) would still like to formulate category theory without use of or reference to set theory. While I admit that I am curious about this for curiosity's sake, I'm not sure if there are any practical motivations for doing this. The only reason for wanting to separate category theory from set theory that I have read about is for the sake of `autonomy of category theory'.


So my question is twofold: What other reasons might categorical foundationalists have for separating category theory from set theory, and what practical purposes might it serve to do this?



Why do categorical foundationalists want to escape set theory?
I don't agree that this is what (most) categorists who are interested in foundations are doing. 


It is true that Lawvere in the mid-60's (and perhaps to this day) wanted to develop a theory of categories independent of a theory of sets, but I don't think that represents the main thrust of modern-day categorical work on "foundations". Much more work has been directed toward developing a full-fledged categorical *theory of sets*, either as in Lawvere's Elementary Theory of a Category of Sets and extensions thereof, or understanding classical theories of sets such as ZF through a categorical lens, as in Algebraic Set Theory. There is also ongoing discussion of what strength of set theory is suitable for doing what category theorists would like to do. As one can see with even a casual perusal of such work, there is no antagonism toward set theory per se, or a desire to somehow get away from sets. 


I think some confusion might stem from over-hasty identification of set theory with a "canonized" form of set theory, such as ZFC (or something in that family such as Gödel-Bernays set theory), based on a single binary predicate called "membership". In ordinary ZFC, a set is characterized by its membership tree, so that the elements of sets are sets themselves, possessing their own internal structure. This may be termed a "materialist" form of set theory (material because elements of sets are considered as having "substance"). If there is antagonism toward this type of set theory on the part of some category theorists, it's because it lends itself to a conception of "set" that is largely irrelevant to the actual practice of core mathematics, insofar as mathematicians don't care what elements are "made of". 


The prevailing trends of mathematical practice today and throughout most of the twentieth century promote a more "structuralist" view: that what counts is not what the elements of a structure "are" particularly, but rather how they are interrelated in a structure, and where two structures are considered abstractly the same if they are isomorphic. This seems like a truism today, but it is precisely this view which drives a more categorically-minded view, which looks toward not what sets "are", but of how we use them, what abstract constructions we want to perform on them, and so on. Thus, concepts such as "power set" are in this view more relevantly captured by suitable universal properties which serve to characterize their structure up to specified isomorphism. A theory of sets which takes this point of view seriously and axiomatically may be termed a "structural set theory". 


Thus the real contrast is between "material" and "structural" theories of sets, with category theorists tending to prefer structural set theory. An example of such is Lawvere's aforementioned Elementary Theory of the Category of Sets (ETCS). A different and more recent example is Mike Shulman's SEAR (Sets, Elements, and Relations), which you can read about at the nLab. 


As for practical benefits of structuralist set theory: they are huge! It should be borne in mind that elementary topos theory was largely inspired by Lawvere's insight that Grothendieck toposes themselves model most of the axioms of the kind of structuralist set theory he was investigating in ETCS, and this has been revolutionary. This answer is already long enough, so I won't enter on a discussion of that here. 


