Here is one further take on the differences of Sets/Categories/Types from the perspective of a mathematician. I think gets at what a practicing mathematician takes under consideration when using one of these three. Key to choosing one of these is the need to handle what equals means.
Summary
- Set Theory: all things are sets; so, x=y is settled by x subset y and y subset x.
- Category theory: objects can be whatever you like but morphisms need to be narrowed to one family (usually sets) and define a composition. So x=y gives way to a pair of inverse morphisms (whatever abstraction morphisms represent, not generally functions).
- Type Theory: data is anything you like, just annotated by a type, functions are primitive logical constructs (e.g. combinators/lambdas) representing actual actions on data, often computationally encodeable. (Non judgemental) Equality is formally added to that Type Theory, often its own type as in Martin-Lof Type Theory, or made explicit by bijective combinators/lambda's. Functions between types are not required to have meaningful compositions to the context at hand, hence are not always categories.
More detail
Logic Feature. Logic considers equality/identity in many ways but in the overlap with mathematics it mostly involves some variation on Leibniz's Law.
x=y if for each property P, P(x) if, and only if, P(y).
Logic Short-coming.
Mathematics strains to know what all P could mean, surely 1+2 looks different to 3 but we want these to be equal "as numbers". So we need some context into which we can say "up to this context equality of this kind makes sense". In math such packing of gets names like "lines", "planes", "sets" "class" "types". In this form, under varied names, the idea could be claimed all the way to Euclid's Elements, but also Des Cartes' introduction of the xy-plane and graphing of functions as what today we write {(x,y)|y=f(x)}. It far form Kantian influence in this root form.
Set Feature.
In ZFC all things are sets. So sets contain other sets and so on. There are paradoxes being avoided by such a treatment, but on the day-to-day working of math this settles the question of equality by the axiom of extensionality.
Set Draw-back.
It strains credulity to assume mathematician view 2, 4/5, pi, and other structures as sets. Mathematicians blithely write sets as {2, 4/5, pi} and know it be different from {3,7,-9} without ever appealing to the ZFC for equality. It is just that when forced to declare that equality makes some sense a mathematician could appeal to some extant sources that modeled all such numbers as sets and thus offer a context for equality. It is not, however, that this is non-constructive or extensional, but rather it is merely hidden, overlooked, or ignored details which could, when necessary, be recovered.
Category Feature.
A principal problem early Category Theory was interested in settling was to allow for refined views of equality, e.g. categories can say two things are isomorphic, or "equivalant" but that meaning exposes explicit mechanisms for translation of data. This view is distinct from Sets where only one mechanism (two-way set inclusion) explains all equality. Categories emphasize how data is made the same. In its first renditions this still depended ultimately on equality in sets as morphisms were captured by sets and this allowed terms like fg=h to be expressed as a set equality. But categories are a recursive algebraic theory (the category of categories makes sense subject to ramification) and these days equality in categories can be refined into higher category expressions instead of depending on sets.
[As a side note, mathematicians might dispute the view of categories as labeled graphs. They are more akin to algebra, in fact they are formally an "essentially algebraic theory" (Peter Fryed). One way to observe this is that graphs are not in general a transitive relation but all category diagrams are required to be so.]
Category Draw-back. Categories, like sets, once more ask the mathematician to translate all their mental models to a new one, one of categories. Even simple structures like numerals and orders are to be recast as diagrams with specific operators of composition and identity. Search for "simplicial sets" and see if that definition improves on the concept of a simplex geoemtricaly for example. So while categories improve on ways to say two things are "isomorphic" or "equivalent", for other things the translation is artificial and forced.
A further issue is the narrowness of morphisms in a category required to enforce composability. For example, the subject of graph theory and more general combiantorics works with such a variety of transformations, often local or inductive studies, which simply do not fit well in categories as the meaning of "a morphism" varies. Even basic concepts like linear algebra do not fit into a single category as we compare matrices (M,N) by formula XM=NY just as often as XMY=N, but the former is an abelian category and the later is not. So these comparisons coexist in the theory but not in the category. So we cannot even study the most useful mathematics without a duplicating the data into multiple categories and then positing how to they should be conjoined after the fact. That makes is less effective as a foundation. Curiously, equality under both such morphisms agrees, suggesting that if focusing just on equals there is a more general foundation to be had.
Type Feature. A principal quality of types to many mathematicians who use it (admittedly few) is that it leaves the data for what it is. It merely annotates (documents) them by labels to inform the reader as what rules and context apply to that data. The user gets to work with the data exactly as she/he/they want. The number pi is a decimal, not a set or an object in a category for example. Equality of pi is as decimal numbers.
Type Draw-back. Letting data be what it is means you loose all the unifications that make math useful. 4/5 is now not strictly equal to 0.80 as these might be annotated by different types (in a Curry type conventions). While Hindley-Milner and others have provided type classes and lattices etc. to unify types it remains an explicit step which can often impede the swifter reasoning afforded by sets at some levels. Univalence takes unification to the extreme closely approximating what can be done with sets. It remains to see if mathematics will accept this approach or come to view it as yet another case where you are forced to translate all your mental models to another form for limited return on investment.
In summary. Mathematicians work in abstraction (in the formal sense of narrowing a topic by rules) and these three foundational models offer ways to do this with some infrastructure. But as those foundations seek to avoid paradoxes and fill gaps they often induce changes in our model which are not actually what we intend. Equality is a place we observe the cracks. This is where the three models a different on a day-to-day level.
