# nLab ETCS

topos theory

foundations

## Foundational axioms

foundational axiom

# Contents

## Idea

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

## Definition

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

###### Definition

The category of sets is the topos which

1. 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 was proposed 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), reprinted as 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)

Erik Palmgren has a constructive predicative variant of ETCS, which can be summarized as: $\mathrm{Set}$ 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 June 5, 2013 23:09:22 by Urs Schreiber (129.173.234.174)