nLab
ETCS

Contents

Idea

The Elementary Theory of the Category of Sets (Lawvere 65), or ETCS for short, is a formulation of set-theoretic foundations in a category-theoretic spirit. As such, it is the prototypical structural set theory.

More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The idea is, first of all, that traditional mathematics naturally takes place “inside” such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the well-pointedness and the axiom of choice but adding the Kock-Lawvere axiom gives a smooth topos inside which synthetic differential geometry takes place.

Modern mathematics with emphasis on concepts of homotopy theory would more directly be founded in this spirit by an axiomatization not just of elementary toposes but of elementary (∞,1)-toposes. This is roughly what univalent homotopy type theory accomplishes – for more on this see at relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes.

Instead of increasing the higher categorical dimension (n,r) in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case (2,2)(2,2) is the elementary theory of the 2-category of categories (ETCC).

Definition

The axioms of ETCS can be summed up in one sentence as:

Definition

The category of sets is the topos which

  1. is a well-pointed topos

  2. has a natural numbers object

  3. and satisfies the axiom of choice.

For more details see

Todd Trimble’s exposition of ETCS

Todd Trimble has a series of expositional writings on ETCS which provide a very careful introduction and at the same time a wealth of useful details.

References

ETCS grew out of Lawvere’s experiences of teaching undergraduate set theoretic foundations at Reed college in 1963 and was originally published in

  • William Lawvere, An elementary theory of the category of sets, Proceedings of the National Academy of Science of the U.S.A 52, 1506-1511 (1965). (pdf)

A more or less contemporary review is

  • C.C. Elgot , Review, JSL 37 no.1 (1972) pp.191-192.

A longer version of Lawvere’s 1965 paper appears in

  • William Lawvere, Colin McLarty, An elementary theory of the category of sets (long version) with commentary, Reprints in Theory and Applications of Categories, No. 11 (2005) pp. 1-35 (TAC)

An undergraduate set-theory textbook using it is

An informative discussion of the pros and cons of Lawvere’s approach can be found in

  • Jean-Pierre Marquis, Kreisel and Lawvere on Category Theory and the Foundations of Mathematics (pdf-slides)

Erik Palmgren has a constructive predicative variant of ETCS, which can be summarized as: SetSet is a well-pointed Π\Pi-pretopos with a NNO and enough projectives (i.e. COSHEP is satisfied). Here “well-pointed” must be taken in its constructive sense, as including that the terminal object is indecomposable and projective.

  • Erik Palmgren, Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets (pdf)

Revised on October 25, 2014 13:42:25 by Urs Schreiber (185.26.182.27)