Return to Answer

There are several articles that I wrote on ETCS, which had originally appeared on the (currently inactive) blog Topological Musings. The nLab articles are nothing more than transcriptions of what I had written into MathML, which is what we use at the nLab. They stop a little short of what you are asking for specifically, so perhaps I can fill the gap now, and say how I think I might have proceeded.

As already mentioned by David and Sridhar, ETCS differs from traditional set theories that are based on a global membership relation (theories whose underlying signature consists of a single binary relation $\in$). Instead, ETCS spells out axioms that one expects to hold for a category of sets and functions. For those who speak the language, the axioms amount to saying that a model of ETCS is a topos with a natural numbers object, such that the terminal set is a generator and the axiom of choice ("epis split") holds.

In this framework, one treats "union" as an operation which internalizes the external operation of taking joins in subset lattices. Thus, if $X$ is a set (or an object if you like), the union operation relative to $X$ is an appropriate morphism

$$\bigcup: PPX \to PX$$

where $PX$ denotes the power set/object of $X$. By the universal property of power objects, this morphism corresponds to a subobject of $X \times PPX$. This subobject is specified by the formula (of an internal language for toposes)

$$\exists_{A: PX} (x \in_X A) \wedge (A \in_{PX} C)$$

where $x$ is of type $X$ and $C$ is of type $PPX$.

There are several ways of doing this, even if one is not familiar with the internal language of a topos. One way, which works for general toposes, proceeds by interpreting the quantifier $\exists_{A: PX}$ directly in terms of image factorizations. Namely, consider the image factorization of the composite

$$[(x \in_X A) \wedge (A \in_{PX} C)] \hookrightarrow X \times PX \times PPX \stackrel{proj}{\to} X \times PPX$$

to get the desired subobject $I \hookrightarrow X \times PPX$. (Of course, this requires that one construct image factorizations in a topos, as treated in any standard text.) The subobject described in brackets is, in turn, a pullback of the form

$$(1_X \times \delta \times 1_{PPX})^\ast(\pi_1^\ast(\in_X) \times \pi_2^\ast(\in_{PX}))$$

where $\in_X \hookrightarrow X \times PX$ and $\in_{PX} \hookrightarrow PX \times PPX$ are the canonical subobjects, where

$$\pi_1: (X \times PX) \times (PX \times PPX) \to X \times PX$$

$$\pi_2: (X \times PX) \times (PX \times PPX) \to PX \times PPX$$

are projection maps, and where $\delta: PX \to PX \times PX$ is the diagonal. Then, as said before, the map $PPX \to PX$ which classifies this image $I \hookrightarrow X \times PPX$ is the desired internal union relative to $X$.

The second way to go is to realize that a model of ETCS is in particular a Boolean topos. Then, if one has already constructed universal quantification (see for instance the second of the three articles in the ETCS series), one can easily interpret the formula

$$\neg \forall_{A: PX} (x \in_X A) \Rightarrow \neg(A \in_{PX} C)$$

once one has defined internal negation, which is not difficult. This circumvents the need to first construct images, but only works in the Boolean case.

However one spells out the details, the larger point is that in ETCS, membership relations are local and relative to objects $X$, in the form of universal subobjects $\in_X \hookrightarrow X \times PX$, as opposed to being given by a single global relation $\in$ that obtains on the class of objects. Correspondingly, set-theoretic operations like union and intersection are also local and relative in this sense. Otherwise, the first-order formulas that specify such operations -- the ones we all know and love -- work pretty much the same way; in ETCS, the relevant operations may be constructed by clever exploitation of universal properties of relations $\in_X$, and not just asserted to exist by way of a comprehension or separation axiom scheme.

There are several articles that I wrote on ETCS, which had originally appeared on the (currently inactive) blog Topological Musings. The nLab articles are nothing more than transcriptions of what I had written into MathML, which is what we use at the nLab. They stop a little short of what you are asking for specifically, so perhaps I can fill the gap now, and say how I think I might have proceeded.

As already mentioned by David and Sridhar, ETCS differs from traditional set theories that are based on a global membership relation (theories whose underlying signature consists of a single binary relation $\in$). Instead, ETCS spells out axioms that one expects to hold for a category of sets and functions. For those who speak the language, the axioms amount to saying that a model of ETCS is a topos with a natural numbers object, such that the terminal set is a generator and the axiom of choice ("epis split") holds.

In this framework, one treats "union" as an operation which internalizes the external operation of taking joins in subset lattices. Thus, if $X$ is a set (or an object if you like), the union operation relative to $X$ is an appropriate morphism

$$\bigcup: PPX \to PX$$

where $PX$ denotes the power set/object of $X$. By the universal property of power objects, this morphism corresponds to a subobject of $X \times PPX$. This subobject is specified by the formula (of an internal language for toposes)

$$\exists_{A: PX} (x \in_X A) \wedge (A \in_{PX} C)$$

where $x$ is of type $X$ and $C$ is of type $PPX$.

There are several ways of doing this, even if one is not familiar with the internal language of a topos. One way, which works for general toposes, proceeds by interpreting the quantifier $\exists_{A: PX}$ directly in terms of image factorizations. Namely, consider the image factorization of the composite

$$[(x \in_X A) \wedge (A \in_{PX} C)] \hookrightarrow X \times PX \times PPX \stackrel{proj}{\to} X \times PPX$$

to get the desired subobject $I \hookrightarrow X \times PPX$. (Of course, this requires that one construct image factorizations in a topos, as treated in any standard text.) The subobject described in brackets is, in turn, a pullback of the form

$$(1_X \times \delta \times 1_{PPX})^\ast(\in_X \times \in_{PX})$$

where $\in_X \hookrightarrow X \times PX$ and $\in_{PX} \hookrightarrow PX \times PPX$ are the canonical subobjects, and where $\delta: PX \to PX \times PX$ is the diagonal. Then, as said before, the map $PPX \to PX$ which classifies this image $I \hookrightarrow X \times PPX$ is the desired internal union relative to $X$.

The second way to go is to realize that a model of ETCS is in particular a Boolean topos. Then, if one has already constructed universal quantification (see for instance the second of the three articles in the ETCS series), one can easily interpret the formula

$$\neg \forall_{A: PX} (x \in_X A) \Rightarrow \neg(A \in_{PX} C)$$

once one has defined internal negation, which is not difficult. This circumvents the need to first construct images, but only works in the Boolean case.

However one spells out the details, the larger point is that in ETCS, membership relations are local and relative to objects $X$, in the form of universal subobjects $\in_X \hookrightarrow X \times PX$, as opposed to being given by a single global relation $\in$ that obtains on the class of objects. Correspondingly, set-theoretic operations like union and intersection are also local and relative in this sense. Otherwise, the first-order formulas that specify such operations -- the ones we all know and love -- work pretty much the same way; in ETCS, the relevant operations may be constructed by clever exploitation of universal properties of relations $\in_X$, and not just asserted to exist by way of a comprehension or separation axiom scheme.

There are several articles that I wrote on ETCS, which had originally appeared on the (currently inactive) blog Topological Musings. The nLab articles are nothing more than transcriptions of what I had written into MathML, which is what we use at the nLab. They stop a little short of what you are asking for specifically, so perhaps I can fill the gap now, and say how I think I might have proceeded.

As already mentioned by David and Sridhar, ETCS differs from traditional set theories that are based on a global membership relation (theories whose underlying signature consists of a single binary relation $\in$). Instead, ETCS spells out axioms that one expects to hold for a category of sets and functions. For those who speak the language, the axioms amount to saying that a model of ETCS is a topos with a natural numbers object, such that the terminal set is a generator and the axiom of choice ("epis split") holds.

In this framework, one treats "union" as an operation which internalizes the external operation of taking joins in subset lattices. Thus, if $X$ is a set (or an object if you like), the union operation relative to $X$ is an appropriate morphism

$$\bigcup: PPX \to PX$$

where $PX$ denotes the power set/object of $X$. By the universal property of power objects, this morphism corresponds to a subobject of $X \times PPX$. This subobject is specified by the formula (of an internal language for toposes)

$$\exists_{A: PX} (x \in_X A) \wedge (A \in_{PX} C)$$

where $x$ is of type $X$ and $C$ is of type $PPX$.

There are several ways of doing this, even if one is not familiar with the internal language of a topos. One way, which works for general toposes, proceeds by interpreting the quantifier $\exists_{A: PX}$ directly in terms of image factorizations. Namely, consider the image factorization of the composite

$$[(x \in_X A) \wedge (A \in_{PX} C)] \hookrightarrow X \times PX \times PPX \stackrel{proj}{\to} X \times PPX$$

to get the desired subobject $I \hookrightarrow X \times PPX$. (Of course, this requires that one construct image factorizations in a topos, as treated in any standard text.) The subobject described in brackets is, in turn, a pullback of the form

$$(1_X \times \delta \times 1_{PPX})^\ast(\pi_1^\ast(\in_X) \times \pi_2^\ast(\in_{PX}))$$

where $\in_X \hookrightarrow X \times PX$ and $\in_{PX} \hookrightarrow PX \times PPX$ are the canonical subobjects, where

$$\pi_1: (X \times PX) \times (PX \times PPX) \to X \times PX$$

$$\pi_2: (X \times PX) \times (PX \times PPX) \to PX \times PPX$$

are projection maps, and where $\delta: PX \to PX \times PX$ is the diagonal. Then, as said before, the map $PPX \to PX$ which classifies this image $I \hookrightarrow X \times PPX$ is the desired internal union relative to $X$.

The second way to go is to realize that a model of ETCS is in particular a Boolean topos. Then, if one has already constructed universal quantification (see for instance the second of the three articles in the ETCS series), one can easily interpret the formula

$$\neg \forall_{A: PX} (x \in_X A) \Rightarrow \neg(A \in_{PX} C)$$

once one has defined internal negation, which is not difficult. This circumvents the need to first construct images, but only works in the Boolean case.

However one spells out the details, the larger point is that in ETCS, membership relations are local and relative to objects $X$, in the form of universal subobjects $\in_X \hookrightarrow X \times PX$, as opposed to being given by a single global relation $\in$ that obtains on the class of objects. Correspondingly, set-theoretic operations like union and intersection are also local and relative in this sense. Otherwise, the first-order formulas that specify such operations -- the ones we all know and love -- work pretty much the same way; in ETCS, the relevant operations may be constructed by clever exploitation of universal properties of relations $\in_X$, and not just asserted to exist by way of a comprehension or separation axiom.

There are several articles that I wrote on ETCS, which had originally appeared on the (currently inactive) blog Topological Musings. The nLab articles are nothing more than transcriptions of what I had written into MathML, which is what we use at the nLab. They stop a little short of what you are asking for specifically, so perhaps I can fill the gap now, and say how I think I might have proceeded.

As already mentioned by David and Sridhar, ETCS differs from traditional set theories that are based on a global membership relation (theories whose underlying signature consists of a single binary relation $\in$). Instead, ETCS spells out axioms that one expects to hold for a category of sets and functions. For those who speak the language, the axioms amount to saying that a model of ETCS is a topos with a natural numbers object, such that the terminal set is a generator and the axiom of choice ("epis split") holds.

In this framework, one treats "union" as an operation which internalizes the external operation of taking joins in subset lattices. Thus, if $X$ is a set (or an object if you like), the union operation relative to $X$ is an appropriate morphism

$$\bigcup: PPX \to PX$$

where $PX$ denotes the power set/object of $X$. By the universal property of power objects, this morphism corresponds to a subobject of $X \times PPX$. This subobject is specified by the formula (of an internal language for toposes)

$$\exists_{A: PX} (x \in_X A) \wedge (A \in_{PX} C)$$

where $x$ is of type $X$ and $C$ is of type $PPX$.

There are several ways of doing this, even if one is not familiar with the internal language of a topos. One way, which works for general toposes, proceeds by interpreting the quantifier $\exists_{A: PX}$ directly in terms of image factorizations. Namely, consider the image factorization of the composite

$$[(x \in_X A) \wedge (A \in_{PX} C)] \hookrightarrow X \times PX \times PPX \stackrel{proj}{\to} X \times PPX$$

to get the desired subobject $I \hookrightarrow X \times PPX$. (Of course, this requires that one construct image factorizations in a topos, as treated in any standard text.) The subobject described in brackets is, in turn, a pullback of the form

$$(1_X \times \delta \times 1_{PPX})^\ast(\pi_1^\ast(\in_X) \times \pi_2^\ast(\in_{PX}))$$

where $\in_X \hookrightarrow X \times PX$ and $\in_{PX} \hookrightarrow PX \times PPX$ are the canonical subobjects, where

$$\pi_1: (X \times PX) \times (PX \times PPX) \to X \times PX$$

$$\pi_2: (X \times PX) \times (PX \times PPX) \to PX \times PPX$$

are projection maps, and where $\delta: PX \to PX \times PX$ is the diagonal. Then, as said before, the map $PPX \to PX$ which classifies this image $I \hookrightarrow X \times PPX$ is the desired internal union relative to $X$.

The second way to go is to realize that a model of ETCS is in particular a Boolean topos. Then, if one has already constructed universal quantification (see for instance the second of the three articles in the ETCS series), one can easily interpret the formula

$$\neg \forall_{A: PX} (x \in_X A) \Rightarrow \neg(A \in_{PX} C)$$

once one has defined internal negation, which is not difficult. This circumvents the need to first construct images, but only works in the Boolean case.

However one spells out the details, the larger point is that in ETCS, membership relations are local and relative to objects $X$, in the form of universal subobjects $\in_X \hookrightarrow X \times PX$, as opposed to being given by a single global relation $\in$ that obtains on the class of objects. Correspondingly, set-theoretic operations like union and intersection are also local and relative in this sense. Otherwise, the first-order formulas that specify such operations -- the ones we all know and love -- work pretty much the same way; in ETCS, the relevant operations may be constructed by clever exploitation of universal properties of relations $\in_X$, and not just asserted to exist by way of a comprehension or separation axiom scheme.