4

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?

3
  • 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 '21 at 6:46
  • Added philosophy of mathematics tag and question.
    – J D
    Nov 23 '21 at 14:02
  • 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 '21 at 15:51
3

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, but still finds popularity among computer language designers. 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.

14
  • 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 '21 at 0:37
  • 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 '21 at 0:39
  • 1
    @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 '21 at 19:56
  • 1
    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 '21 at 19:57
  • 1
    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 '21 at 20:07
1

(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 '21 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 '21 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.