### An Elementary Theory of the Category of Sets

#### Posted by Emily Riehl

*Guest post by Clive Newstead*

William Lawvere’s Elementary Theory of the Category of Sets (ETCS) was one of the first attempts at using category theory as a foundation of mathematics and formulating set theory in category theoretic language. In this post I will outline the content of Lawvere’s paper [Lawvere 1965] and put it in a historical context; suggestions for further reading are at the end. Before I begin, I’d like to thank Emily Riehl, Steve Awodey and the other Kan Extension Seminar participants for their helpful feedback, suggestions, and reading responses to the paper; and, of course, William Lawvere for writing it!

### Some history

ETCS came about at a boomtime for category theory and the foundations of mathematics. It was the early 1960s; category theory had found its feet and had started being used extensively throughout mathematics, notably in algebraic geometry with the work of Alexander Grothendieck. Around the same time, Paul Cohen developed the technique of forcing, which has since become central to modern set theory. Lawvere had recently written his Ph.D. thesis [Lawvere 1963], which was the first step in his programme of using the category of categories as a foundation. It was therefore fitting that he should want to try his hand at doing set theory inside category theory.

Lawvere’s attempt did not go unopposed, even by the likes of Samuel Eilenberg and Saunders Mac Lane:

His attempt to explain this idea to Eilenberg did not succeed; […] Sammy asked me to listen to Lawvere’s idea. I did listen, and at the end I told him “Bill, you can’t do that. Elements are absolutely essential to set theory.” [Mac Lane 1988]

Unfazed, Lawvere pressed on and in 1964 he published the ETCS paper, which was expanded and reprinted in 1965. What follows is a very brief sketch of its contents; more depth and technical details can be found in the paper itself.

### Axioms of ETCS

Before listing the axioms, we should fix some set theoretic notation with category theoretic meaning: given an object $A$ in a category with a terminal object $1$, if $a \colon 1 \to A$ then we write $a \in A$ and say $a$ is an *element* of $A$. If $s \colon S \to A$ is monic then we say $s$ is a *subset* of $A$, and write $s \subseteq A$. We then write $a \in s$ if $a$ factors through $s$.

The axioms of ETCS consist of the usual axioms for a category $\mathcal{C}$ together with the following eight axioms:

- $\mathcal{C}$ has an initial object $0$, a terminal object $1$, products $A \times B$ and coproducts $A+B$ of all pairs $A,B$, and equalisers and coequalisers of all pairs $f,g : A \rightrightarrows B$. (Thus $\mathcal{C}$ has all finite limits and colimits.)
- Every pair of objects $A,B$ has an exponential $B^A$.
- $\mathcal{C}$ has a natural numbers object $\mathbb{N}$, with zero morphism $\mathtt{zero} : 1 \to \mathbb{N}$ and successor morphism $\mathtt{suc} : \mathbb{N} \to \mathbb{N}$.
- $\mathcal{C}$ is well-pointed, i.e. given any pair of maps $f,g : A \rightrightarrows B$ with $f \ne g$, there is an element $a \in A$ such that $f \circ a \ne g \circ a$.
- Axiom of Choice: If $f : A \to B$ and there is some $a \in A$, then there exists a
*quasi-inverse*$g : B \to A$, which satisfies $f \circ g \circ f = f$. - If $A$ has no elements then $A$ is an initial object.
- If $a \in A + B$ then $a$ factors through one of the coproduct inclusions.
- $\mathcal{C}$ has an object with more than one element.

With modern technology we can simplify this list considerably: a model of ETCS is a well-pointed topos with a natural numbers object satisfying the axiom of choice.

In Lawvere’s paper, the axioms are introduced as they are needed, rather than all as one list. As such, it becomes clear which properties held by the category of sets are also held by other categories. Moreover, Lawvere comments on how the axioms interact with each other. For example, since the category $\mathbf{Pos}$ of posets and order-preserving maps satisfies each of the axioms except for #5, the axiom of choice is independent of the other axioms of ETCS.

### Mathematics with ETCS

Lawvere demonstrated the usefulness of ETCS as a set theory by proving six mathematical theorems.

**Theorem 1 (Primitive recursion).** Given a pair of morphisms
$f_0 : A \to B, \quad u : \mathbb{N} \times A \times B \to B$
there is a morphism $f : \mathbb{N} \times A \to B$ satisfying, for each $n \in \mathbb{N}$ and $a \in A$,
$f \circ \langle \mathtt{zero}, a\rangle = f_0 \circ a, \quad f \circ \langle \mathtt{suc} \circ n, a \rangle = u \circ \langle n, a, f \circ \langle n, a \rangle \rangle$

The primitive recursion theorem requires only axioms 1-3, and uniqueness of $f$ is implied by axiom 4. Thus primitive recursion can be done in categories such as the functor category $[\mathbb{C}, \mathbf{Set}]$ for any small category $\mathbb{C}$, and in the arrow category $\mathbf{Set}^{{\rightarrow}}$.

**Theorem 2 (Peano’s postulates).**

- The morphism $\mathtt{succ} : \mathbb{N} \to \mathbb{N}$ is monic
- If $n = \mathtt{succ} \circ m$ for some $m \in \mathbb{N}$ then $n \ne \mathtt{zero}$.
- If $s \subseteq \mathbb{N}$ and $n \in s \Rightarrow \mathtt{succ} \circ n \in s$ then $s = \mathrm{id}_{\mathbb{N}}$.

The third of these allows us to perform mathematical induction in any model of ETCS.

**Theorem 3 (Image factorization).** Every morphism can be factored as an epi followed by a mono.

**Theorem 4 (Unions).** Let $2 = 1+1$ and let $\top : 1 \to 2$ be one of the inclusion maps. Given any $\alpha : I \to 2^A$ there is a subset $u : {\bigcup_{\alpha}} \to A$ such that, for all $a \in A$, $a \in u$ if and only if $\mathtt{ev}_{2^A} \circ \langle \alpha \circ j, a \rangle = \top$ for some $j \in I$.

Intuitively, $\bigcup_{\alpha}$ is the union of the subsets of $A$ picked out by the indexing morphism $\alpha$; that is, ${\bigcup_{\alpha}} = \bigcup_{j \in I} \alpha(j)$

**Theorem 5 (Complements).** Let $A$ be an object. Given any subset $s : S \to A$ there is a subset $s' : S' \to A$, such that $A \cong S+S'$ with $s$ and $s'$ as the coproduct injections.

**Theorem 6 (Quotients).** Let $A$ be an object and $f = \langle f_0, f_1 \rangle : R \to A \times A$ be an equivalence relation. Let $\pi_0, \pi_1: A \times A \to A$ be the product projections. Then $f$ is the equaliser of $q \circ \pi_0$ and $q \circ \pi_1$, where $q : A \to Q$ is the coequaliser of $f_0$ with $f_1$.

Intuitively, $Q$ is the quotient of $A$ by $R$, then the theorem is stating that $R$ is precisely the set of pairs $\langle a,b \rangle \in A \times A$ such that $[a]_R = [b]_R \in Q$.

### Metamathematics

The paper closes with a theorem justifying that the axioms of ETCS really do characterise categories which are sufficiently ‘like’ the category of sets. Lawvere refers to this likeness as the *invariant form* of the category of sets.

**(Meta)theorem.** If $\mathcal{C}$ is a locally small, complete model of ETCS, then $\mathcal{C}$ is equivalent to $\mathbf{Set}$.

The equivalence $\mathcal{C} \overset{T}{\underset{\check T}{\rightleftarrows}} \mathbf{Set}$ is given by $TA = \text{Hom}_{\mathbf{Set}}(1,A) = \{ \text{elements of } A \}$ $\check{T}X = \sum_{x \in X} 1$

### What happened next?

The appeal of ETCS was not felt by the mathematical community at the time. Indeed, according to Marquis and Reyes:

The category of sets was not taken as a foundational framework. It was not studied and explored. […] It seems that one of the most common reactions at the time was that ETCS was merely a translation in categorical terms of the standard axioms of set theory [Marquis and Reyes 2011]

Even Lawvere acknowledged the shortcomings of his work:

However, it is the author’s feeling that when one wishes to go substantially beyond what can be done in the theory presented here, a much more satisfactory foundation for practical purposes will be provided by a theory of the category of categories.

However, the impact of ETCS stems not from its (non-)use as a foundation, but from the research that it led to. It was one of the first attempts to give a categorical account of logic, and it led directly to the definition of an elementary topos, which generalised the notion of a Grothendieck topos and bridged the gap between geometry and logic via category theory. For a number of reasons it was toposes, rather than models of ETCS, which became the central object of study in categorical logic.

### References and suggested reading

- Lawvere, F.W.
*Functorial Semantics of Algebraic Theories*, Ph.D. thesis, Columbia University (1963). - Lawvere, F.W. An elementary theory of the category of sets,
*Proceedings of the National Academy of Science of the USA*52, 1506-1511 (1965), reprinted as Lawvere, F.W., McLarty, C. 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. - Mac Lane, S. Concepts and categories in perspective. In
*A Century of Mathematics in America, I*, vol. I, pages 323-365. American Mathematical Society, Providence (1988). - Marquis, J.-P. and Reyes, G.
*The History of Categorical Logic: 1963-1977*. In*Handbook of the history of logic*, vol. 6, pp. 689-800. Elsevier (2011).

## Re: An elementary theory of the category of sets

Clive, thank you for this fantastic summary!

I’m hoping that we can use the comments, not just for the broader philosophical/historical/conjectural conversation that the $n$-Category Café excels at, but also to provide a space to ask and answer smaller questions raised by the paper itself, for those who want to read along with the seminar. I’ll start:

In Remark 5 on the top of page 28, Lawvere mentions three power-set functors, which surprised me, because I was only aware of two.

The contravariant power-set functor is the easiest: it’s immediate from the parametrized adjunction defining the exponentials.

In set-builder notation, the (usual) covariant power-set functor, applied to a map $f \colon A \to B$, takes $S \subset A$ to

$f_!(S) := \{ b \in B \mid \exists s \in S, f(s)=b\}.$

This is what Lawvere describes categorically on the previous page.

I believe that the third power-set functor (also covariant), when applied to $f \colon A \to B$, should take $S \subset A$ to

$f_*(S) := \{ b \in B \mid f^{-1}(b) \subset S\}.$

With some work I’m sure this map $2^A \to 2^B$ can be constructed in ETCS, but let me decline to do this right now.

The reason I think this is right is that I remember from somewhere in Peter Johnstone’s topos theory lecture notes that $f_!$, $f^*$ (meaning precomposition), and $f_*$ should be

`adjoints.'' Interpreting`

adjoint” with respect to the posets of subobjects of $A$ and $B$, I think this is right: we have $f^*(T) \subset S$ if and only if $T \subset f_*(S)$, which says that $f^* \dashv f_*$.What I don’t see (quoting Remark 5), is how $f_*$ is

Can someone clarify?