# nLab ETCS

### Context

#### Topos Theory

Could not include topos theory - contents

foundations

## Foundational axioms

foundational axiom

# Contents

## Idea

The Elementary Theory of the Category of Sets , or ETCS for short, is an axiomatic formulation of set theory in a category-theoretic spirit. As such, it is the prototypical structural set theory. Proposed shortly after ETCC in (Lawvere 65) it is also the paradigm for a categorical foundation of mathematics.1

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.

## 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

## A contemporary perspective

Modern mathematics with its emphasis on concepts from homotopy theory would more directly be founded in a similar 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)$ is the elementary theory of the 2-category of categories (ETCC).

## A Constructive View

Erik Palmgren (Palmgren 2012) has a constructive predicative variant of ETCS, which can be summarized as:

$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.

## 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 pp.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 11 (2005) pp. 1-35. (TAC)

An undergraduate set-theory textbook using it is

A short overview article:

• Tom Leinster, Rethinking set theory arXiv

On the anticipation of ‘structural sets’ in Cantor:

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

Palmgren’s ideas can be found here:

• Erik Palmgren, Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets , Ann. Pure. App. Logic 163 no.10 (2012) pp.1384-1399. (pdf)

For the relation between the theory of well-pointed toposes and weak Zermelo set theory as elucidated by work of J. Cole, Barry Mitchell, and G. Osius in the early 1970s see

• Peter Johnstone, Topos Theory , Academic Press New York 1977 (Dover reprint 2014). (sections 9.2-3)

• Barry Mitchell, Boolean Topoi and the Theory of Sets , JPAA 2 (1972) pp.261-274.

• Gerhard Osius, Categorical Set Theory: A Characterization of the Category of Sets , JPAA 4 (1974) pp.79-119.

1. For a careful comparative discussion of its virtues as foundation see foundations of mathematics or the texts by Todd Trimble referred to below.

Revised on March 20, 2015 01:45:07 by Bas Spitters (108.17.80.235)