10

IIRC, in the univalent-foundations program (per Voevodsky), category theory is represented as a possible sort of evolution or new wave of type theory. Maybe my memory is off, but anyway, in nlab they say:

Type theory and certain kinds of category theory are closely related. By a syntax-semantics duality one may view type theory as a formal syntactic language or calculus for category theory, and conversely one may think of category theory as providing semantics for type theory. The flavor of category theory used depends on the flavor of type theory; this also extends to homotopy type theory and certain kinds of (∞,1)-category theory.

Also, again IIRC, the choice of name for category theory referred back to Aristotelian/Kantian usage of categories. Suppose that sets are representatives of extension, whereas types are representatives of intension. (Sorry, couldn't find a more specific citation.) In, say, Kantian terms, the categories, being on the side of cognition that is discursive, would therefore be intensional functions. That they would be typomorphic(?) seems to readily follow, at least according to the supposition I just made earlier in this paragraph.

All that being said, for some reason, to me, there is something intuitively different about category theory vs. type theory. AFAIK, type theory was tried out as an alternative foundations of mathematics, but fell to set theory. By contrast, category theory is a to date quite successful picture of an alternative foundations of mathematics.†

Is this because categories are not types? What I was thinking was: a term refers to a set if the reference has elements; a term refers to a type if the reference has tokens (I appreciate that the tokenhood relation does not appear in type theory proper as it does in this other understanding of typology); but if a term's reference has elements and tokens, then that term refers to a category. So what type theory lacks, namely a well-founded theory of extensionality, is made up for by this category-theoretic duality. Then category theory can import the seemingly mathematical qualities of type theory, into the music of its notation, alongside the set-theoretic semiosis, and it would therefore easily seem to supersede unadorned set theory, as a foundation of mathematics.

My only objection at this stage would be to say: in the end, typological functions advert more to the logical sphere††; the distinctly mathematical content of a category is all carried by the elementhood facts that the category figures in. In this sense, the viability of category theory as a sufficiently justified alternative foundation of mathematics, is only an illusion. In all honesty, I actually believe that this objection is true.

This is perhaps ironic, given that Kantian usage of categories initially motivated this whole new(?) genre of mathematics: according to Kant, after all, we need pure extensional objects (space and time) to adequately ground our mathematics; the bare notion of extensionality wouldn't do (in other words, the intensionality of the term extension is not a sufficient basis for justifiable mathematics).

††The logical elasticity of typology being, then, an analogue or complement of logical pluralism.

How do philosophers of mathematicians understand the differences between set, type, and category theory?

8
  • 1
    Hmm. I'll need to think more about this, but on "a well-founded theory of extensionality[,] is made up for by this category-theoretic duality", I don't think this is right. Part of the point of Type theory a la Church is building something like extensionality in from the start to avoid inconsistency - the "extension" of a type is the terms of that type, and terms only have one type. There isn't a straightforward "extension iterator" within the theory, but I don't think Univalence requires this as long as there is some kind of type identity condition.
    – Paul Ross
    Nov 23, 2021 at 6:46
  • Added philosophy of mathematics tag and question.
    – J D
    Nov 23, 2021 at 14:02
  • 1
    The short difference is types are essentially sets that don't lead to paradox and emphasize membership; categories are essentially directed graphs that emphasize mappings. Sets are iterative hierarchical constructions, and categories are functional structures. Both theories are expressed with logical statements, and are two different ways of seeing and doing math.
    – J D
    Nov 23, 2021 at 15:51
  • Mathematicians seem confused about the differences. A math book on categories begins (or has an appendix) on ZFC/NBG or in modern times a Type Theory. A book on sets often implements a form of simple type theory to get some functions and ordered pairs to start with. Then books on types appeal to categories as models in support of axioms they want to impose. If the average mathematician has a uniform philosophy here it is that they assume someone knows the differences and confirmed it all works. That (unfounded) trust lets them use any one of these as it suits them.
    – Algeboy
    Nov 16, 2022 at 17:38
  • 1
    @Algeboy in my current writing project, I have ended up using the intension/extension distinction as the relevant primitive distinction. I've run into trouble with types having occurrences and tokens, but either Zalta's encoding/instantiating distinction or/and the multiset element/multiplicity distinction then pick up some slack. Best I can do for now 😕 Nov 16, 2022 at 17:53

3 Answers 3

12

Short Answer

It sounds you're struggling to understand the relationship between three fundamental theories. Naive set theory is the theory used historically by Gottlob Frege to show that all mathematics reduces to logic. Type theory was proposed and developed by Bertrand Russell and others to put a restriction on set theory to avoid Russell's paradox, and which was then replaced by ZF and ZFC. And category theory has been offered as an alternative to ZFC as a foundational theory, which is powerful in analyzing the functional aspects of mathematical structures and might be seen as an abstraction of set theory. All three theories are related to what Wikipedia calls the Curry–Howard–Lambek correspondence which purports to show how proofs, programs, and category-theoretic are isomorphisms of a sort, and which suggests a deeper interconnectedness between the three.

Long Answer

Sets and Their Problems

There are many theories of math, but set theory (ST), type theory (TT), and category theory (CT) are important because they raise foundational questions and are considered fundamental theories. Naive set theory, for instance, can be used to define numbers and arithmetic. A famous example is von Neumann Ordinals. From Georg Cantor and the use of set theory, the argument actual infinities exist has been made. The problem with naive set theory is that it is possible to derive a contradiction as Russell showed Frege, now known as Russell's paradox. The response led by Russell was to come up with a new system to replace naive set theory, and what he put forth were a series of theories that allow for types. From Linnebo's Philosophy of Mathematics, p. 143:

Gödel goes so far as to claim that set theory is "nothing else but a natural generalization of the theory of types, or rather, it is what becomes of the theory of types if certain superfluous restrictions are removed... One of the "superfluous restrictions" that Gödel has in mind...[is] type theory cannot allow an individual to be a member of a clan directly but only via some family".

The short version is type theory escapes Russell's paradox by creating a strict hierarchy of "sets" so a set cannot be a member of itself which is a presumption that leads to the paradox. For both historical and technical reasons, however, mathematicians chose ZF theory and developed it, eventually accepting an axiom of choice, or others extending it, like in NBG:

Zermelo–Fraenkel set theory is intended to formalize a single primitive notion, that of a hereditary well-founded set, so that all entities in the universe of discourse are such sets. Thus the axioms of Zermelo–Fraenkel set theory refer only to pure sets and prevent its models from containing urelements (elements of sets that are not themselves sets). Furthermore, proper classes (collections of mathematical objects defined by a property shared by their members where the collections are too big to be sets) can only be treated indirectly. Specifically, Zermelo–Fraenkel set theory does not allow for the existence of a universal set (a set containing all sets) nor for unrestricted comprehension, thereby avoiding Russell's paradox. Von Neumann–Bernays–Gödel set theory (NBG) is a commonly used conservative extension of Zermelo–Fraenkel set theory that does allow explicit treatment of proper classes.

An Alternative of Objects and Maps

Category theory is another matter completely, and was invented specifically with looking for generalization among mathematical structures. From WP:

Category theory formalizes mathematical structure and its concepts in terms of a labeled directed graph called a category, whose nodes are called objects, and whose labelled directed edges are called arrows (or morphisms).1 A category has two basic properties: the ability to compose the arrows associatively, and the existence of an identity arrow for each object. The language of category theory has been used to formalize concepts of other high-level abstractions such as sets, rings, and groups. Informally, category theory is a general theory of functions... Samuel Eilenberg and Saunders Mac Lane introduced the concepts of categories, functors, and natural transformations from 1942–45 in their study of algebraic topology, with the goal of understanding the processes that preserve mathematical structure.

Unlike thinking about the foundations as sets or collections, categorical-theoretic thinking conceives the world of mathematical abstract objects as objects and maps. This lends the theory quite nicely to expression graphically as mathematical graphs. Instead of membership and equivalence as the important relations, mappings and order are seen as primary. Its theoretical defenders believe that this shows mathematics better:

From Conceptual Mathematics: A First Introduction to Categories, p.3:

Our goal in this book is to explore the consequences of a new and fundamental insight about the nature of mathematics which has led to better methods for understanding and using mathematical concepts... While this idea, that mathematics involves different categories and their relationships, has been implicit for centuries, it was not until 1945 that Eilenberg and Mac Lane gave explicit definitions... synthesizing many decades of analysis of the working of mathematics and the relationships of its parts.

Summary

You are correct that set theory, type theory, and category theory are very important to mathematics as part of a philosophical challenge, and all have some relation to foundational questions. Remember that the foundations of mathematics is very important to explain what math 'is', which is contested among philosophers of mathematics. Logicists, formalists, empiricists, nominalists, and others have very different view of what math is and whether or not abstract objects are objective, real, and so on. One good place to get started is 'Philosophy of Mathematics' (SEP). Remember that set theory (by way of ZFC) is important to the logicist program, and category theory appeals to structuralists; both the question of 'what mathematics is' is still a contested question.

17
  • 2
    I appreciate the effort you put into your reply; however, some of your remarks seem off the mark. This isn't in the reply itself, but a comment of yours: "Sets are iterative hierarchical constructions." However, this is only true of the iterative hierarchy, and does not speak to looping sets or infinite descending elementhood chains (nonwell-founded set theory). Moreover, logicism historically diverged from set theory, in that the axiomatic method in set theory was built off the recognition that the logicist program (at least at the time) was unsuccessful at reducing math to logic. Nov 24, 2021 at 0:37
  • 2
    Now, this isn't anything you said that I directly disagree with, but you mention category theory as involving, for all intents and purposes, graph theory. And the semantics(?) of Aczel's nonwell-founded set theory, for instance, has it that sets are accessible pointed graphs. So do these approaches involve reducing mathematics to graph theory? Why would graph theory be so privileged? Nov 24, 2021 at 0:39
  • 3
    @KristianBerry Thank you! I have to confess, I am trying to convert you to a psychological approach to mathematics, so if I'm unabashed in what might be seen as unorthodoxy, I claim full credit. :D I do want to spread what I believe to be a practically unrecognized mathematical philosophy that starts in Where Mathematics Comes From, but extends much deeper into an alternative semantical theory. I think the philosophy that undergirds this book is the inheritor of Kant's TI. But if you'll have none of it and constructivism, cool.
    – J D
    Nov 24, 2021 at 19:56
  • 2
    And if you ever want to learn calc, hit me up. My license has expired, but I still remember a few things.
    – J D
    Nov 24, 2021 at 19:57
  • 2
    Although my epistemological beliefs draw heavy inspiration from Kant, he seems not to have adequately solved the problem of the regress of reasons. The solution to this problem that I do accept, has led me to accept virtually the entire large-cardinal program in mainstream set theory, with some quirks. So at the end of the day, a theory of mathematics that doesn't lead to the higher infinite, I find seriously deficient (which isn't to say that intuitionistic/constructivist large cardinals are necessarily impossible...). Nov 24, 2021 at 20:07
3

(Disclaimer: Long time ago, I worked practically within the CS field, namely, with programming languages based on category theory (Haskell, OCaml). So, I might be wrong, but I will present my common-sense two cents, based off my intuitions)

The way I see it, category theory is a theory that is founded on a type theory. It goes beyond type theory as it bases its assumptions on the criteria of composability, and identity. In short, the category is about morphisms (structure-preserving "mappings") between categories. It implements structure-preserving functions between different categories, i.e. mapping, chaining, or joining different category objects.

Type theory is more fundamental in my view. It relates to a type system that gives meaning to which operations can be performed on a given entity, but doesn't necessarily implement the operations themselves.

Category theory typically uses a type system that is applied to its object nodes. The type theory does not, by itself, posit such concrete objects along with the mappings. In my view, type theory is more abstract than that. Type theory is an internal language of category theory. For instance, in category theory, you have implemented types like Functor, Setoid, Monad. So, the category theory is a particular type system but type theory can be widely used to implement any such other system.

Type_theory#Relation_to_category_theory

As John Lane Bell writes: "In fact categories can themselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax."

2
  • Im upvoting bc the link is a solid find!
    – J D
    Nov 23, 2021 at 15:54
  • I do wonder if categories can't serve as a basis for types. : ) It would introduce a certain fun circularity, wouldn't it?
    – J D
    Nov 23, 2021 at 15:55
1

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.

1
  • Type theory, logic, and category theory are connected. Specifically, every logic yields a category, every type theory yields a category of categories, and every logic yields a category of categories. This connection is called categorical logic. A better approach would be to try to situate type theories and logics on one side of a syntactic-semantic divide, with categories on the other side, as is done in the standard tripartite presentation.
    – Corbin
    Jul 13, 2023 at 6:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .