I highly recommend this paper by Tom Leinster. It is quite a nice paper showing how category bigots do set theory—while skipping the category theory. It is well thought out and well written. I consider it a plug for categories as it describes why it is in fact a good idea apart from category theory. The paper omits an important feature of ZFC: Constructing integers, reals etc. from sets provides a consistency proof relative to set axioms. Such constructs also serve as a concrete conceptual images of the real line which may be useful in some cases. I have not yet learned how the category student is to learn of the reals.

Here is Leinster’s version of the Category people’s foundation for set theory. Whereas ZFC talks of only sets, XX (as I will call his theory) has two sorts of things: sets and functions. Sets are written in upper case letters and functions in lower case. There is a primitive predicate of a function f and two sets X and Y. It is written “f : X → Y”. That there are two sorts which each use their own set of variables (like Fortran in 1956) is no real problem for first order predicate calculus which usually admits just one sort. Here I describe why two sorted logic is no deal stopper.

There is one more primitive, a function of two functions, yielding another function. (Composition if you must know.) It is well known how to include functions within a strict predicate calculus system: a predicate F which says of three functions f, g, h that f = f°h.


Lawvere’s Category Sets, thereon, perspectives