After reading this essay about the history of type theory, I have refined my assessment of the set- vs. type-theory question in two ways. More similarly to what I was thinking before, I still ground the distinction in a function from extensionality vs. intensionality, only now let E be extensionality and I intensionality, and say:
- A theory is a set theory if its referents are such that E is prior to (but not to the exclusion of) I.
- A theory is a type theory if I comes before E.
- A theory is a category theory if neither E nor I is prior (or, more finely, category theory ranges over (1) and (2) but also (3), and it is this disjunctive generality that distinguishes it from its compatriots).
However, I had a very different intuition about the question at the same time based on the issue of "the foundations of mathematics." From this viewpoint, the difference between set theory and category theory is more a historical difference in responses to the "foundations" problem. To quote the SEP article on category theory:
When used to characterize a specific mathematical domain, category theory reveals the frame upon which that area is built, the overall structure presiding to its stability, strength and coherence. The structure of this specific area, in a sense, might not need to rest on anything, that is, on some solid soil, for it might very well be just one part of a larger network that is without any Archimedean point, as if floating in space. To use a well-known metaphor: from a categorical point of view, Neurath’s ship has become a spaceship.
Still, it remains to be seen whether category theory should be “on the same plane,” so to speak, as set theory, whether it should be taken as a serious alternative to set theory as a foundation for mathematics, or whether it is foundational in a different sense altogether. [emphasis added]
Set theory arose in connection with a belief that mathematics has "foundations," expresses this belief in axiomatic methodologies, and crystallizes this theme in the very axiom of foundation itself, which delivers the one and only V = X sentence that is fundamentally confirmed within the ZFC framework, viz. V = WF (where WF is the proper class of well-founded sets). (I say "within the framework" to note that proper-class theory does go beyond strict ZFC, but conservatively, at least if one uses a reserved proper-class theory.) (V = WO, or all the well-ordered sets, is also given, except that the choiceless hierarchy raises a red flag over this equation; so at least we would say that ZF, not full ZFC, only justifies V = WF. Hence the qualifier "fundamentally" for the confirmation in play.)
Type theory, though, too has a foundationalistic theme, both in terms of what it was/is used for (again, in attempts to "found" mathematics), and in its preoccupation with avoiding impredicative objects. But category theory does not seem so "limited." For a generic category theorist, it seems possible to imagine that many or even all categories are coherentistically related from the outside; some categories are internally foundationalistic, proceeding from initial objects via well-founded sequences of morphisms to the ambivalent ramification of the theory internal to such categories. But a category as a whole might admit of cofoundational relations instead (or there might even be a Lawverean "category of categories" with itself as one of its own objects; though see about n-categories for how the Lawverean theme can be played in a way that sounds like the song of ramified type theories with their evasion of unrestricted quantification).
Graph-theoretically, one might imagine scattered looping structures from some of whose nodes one can track metaloops (loops between loops), although one could also imagine some internally non-looping structures connected to other non-looping structures by external cofoundational relations. This "looks like" Susan Haack's analogy of the crossword puzzle as an intuitive display of the foundherentist thesis: individual WF-sequences, as well as local loops, are like the solvable entries in such a puzzle, and the maps between sequences/loops are like the intersections of solvable entries.
Perhaps this question has a trivial or obvious answer: yes, category theory is more coherentistic than set theory has tended to be. But this is historically contingent in that there are coherentistic moments in mainline set theory anyway (e.g. Gödel's doctrine of extrinsic justifiers), and so though set theorists were stereotypically hostile to parafoundational objects (e.g. Penelope Maddy dismisses the relevance of parafoundational sets from her assessment of "maximizing isomorphism types"), this hostility has of late been more allayed and anyway, we're ever on the lookout for ways to translate such theories into the "format" of other theories. This connects up with the algebraism whose children are the thematics of category theory to this day, perhaps.
Can the difference between set theory and category theory (but then to a rather lesser extent type theory) be traced less to abstract, internal definitions of these kinds of theories, and more to historical contingencies related to individual human set/category theorists' attitudes towards the "foundations of mathematics" question?
Addendum. Other evidence/argument: consider the apparent difference in attitude towards logic, between normal set theorists and category theorists. Category theory involves the method of translating systems into each other, which is a very coherentistic method (one does not foundationalistically justify a theory by showing that it can be expressed by many-sorted, second-order, and plurally-quantified logic, say; or by shuffling to and from algebraic representations of a theory). More pointedly, the diversity of logics is extremely operational for category theory, whereas a normal (or classical) set theorist is at pains to rest in the sanctuary of a specific logic, for the purposes of showcasing their ideas. So in other words, set theorists tend to treat "logic" as a count noun only (philosophically sensitive/up-to-date set theorists, like Hamkins, recognize the broader possibility, however), while category theorists appreciate that "logic" can be effectively used as a count noun and a mass noun. (This is faithful to English, at least: we do not say that a person who uses a good argument is "many logical" compared to someone who relies on blind fideism, but "more logical," or we can say "much more logical" but not "much logical.")
