ETCS: Building joins and coproducts

After a long hiatus, I’d like to renew the discussion of axiomatic categorical set theory, more specifically the Elementary Theory of the Category of Sets (ETCS). Last time I blogged about this, I made some initial forays into “internalizing logic” in ETCS, and described in broad brushstrokes how to use that internal logic to derive a certain amount of the structure one associates with a category of sets. Today I’d like to begin applying some of the results obtained there to the problem of constructing colimits in a category satisfying the ETCS axioms (an ETCS category, for short).

(If you’re just joining us now, and you already know some of the jargon, an ETCS category is a well-pointed topos that satisfies the axiom of choice and with a natural numbers object. We are trying to build up some of the elementary theory of such categories from scratch, with a view toward foundations of mathematics.)

But let’s see — where were we? Since it’s been a while, I was tempted to review the philosophy behind this undertaking (why one would go to all the trouble of setting up a categories-based alternative to ZFC, when time-tested ZFC is able to express virtually all of present-day mathematics on the basis of a reasonably short list of axioms?). But in the interest of time and space, I’ll confine myself to a few remarks.

As we said, a chief difference between ZFC and ETCS resides in how ETCS treats the issue of membership. In ZFC, membership is a global binary relation: we can take any two “sets” and ask whether . Whereas in ETCS, membership is a relation between entities of different sorts: we have “sets” on one side and “elements” on another, and the two are not mixed (e.g., elements are not themselves considered sets).

Further, and far more radical: in ETCS the membership relation is a function, that is, an element “belongs” to only one set at a time. We can think of this as “declaring” how we are thinking of an element, that is, declaring which set (or which type) an element is being considered as belonging to. (In the jargon, ETCS is a typed theory.) This reflects a general and useful philosophic principle: that elements in isolation are considered inessential, that what counts are the aggregates or contexts in which elements are organized and interrelated. For instance, the numeral ‘2’ in isolation has no meaning; what counts is the context in which we think of it (qua rational number or qua complex number, etc.). Similarly the set of real numbers has no real sense in isolation; what counts is which category we view it in.

I believe it is reasonable to grant this principle a foundational status, but: rigorous adherence to this principle completely changes the face of what set theory looks like. If elements “belong” to only one set at a time, how then do we even define such basic concepts as subsets and intersections? These are some of these issues we discussed last time.

There are other significant differences between ZFC and ETCS: stylistically, or in terms of presentation, ZFC is more “top-down” and ETCS is more “bottom-up”. For example, in ZFC, one can pretty much define a subset by writing down a first-order formula in the language; the comprehension (or separation) axiom scheme is a mighty sledgehammer that takes care of the rest. In the axioms of ETCS, there is no such sledgehammer: the closest thing one has to a comprehension scheme in the ETCS axioms is the power set axiom (a single axiom, not an axiom scheme). However, in the formal development of ETCS, one derives a comprehension scheme as one manually constructs the internal logic, in stages, using the simple tools of adjunctions and universal properties. We started doing some of that in our last post. So: with ZFC it’s more as if you can just hop in the car and go; with ETCS you build the car engine from smaller parts with your bare hands, but in the process you become an expert mechanic, and are not so rigidly attached to a particular make and model (e.g., much of the theory is built just on the axioms of a topos, which allows a lot more semantic leeway than one has with ZF).

But, in all fairness, that is perhaps the biggest obstacle to learning ETCS: at the outset, the tools available [mainly, the idea of a universal property] are quite simple but parsimonious, and one has to learn how to build some set-theoretic and logical concepts normally taken as “obvious” from the ground up. (Talk about “foundations”!) On the plus side, by building big logical machines from scratch, one gains a great deal of insight into the inner workings of logic, with a corresponding gain in precision and control and modularity when one would like to use these developments to design, say, automated deduction systems (where there tend to be strong advantages to using type-theoretic frameworks).

Enough philosophy for now; readers may refer to my earlier posts for more. Let’s get to work, shall we? Our last post was about the structure of (and relationships between) posets of subobjects relative to objects , and now we want to exploit the results there to build some absolute constructions, in particular finite coproducts and coequalizers. In this post we will focus on coproducts.

Note to the experts: Most textbook treatments of the formal development of topos theory (as for example Mac Lane-Moerdijk) are efficient but highly technical, involving for instance the slice theorem for toposes and, in the construction of colimits, recourse to Beck’s theorem in monad theory applied to the double power-set monad [following the elegant construction of Paré]. The very abstract nature of this style of argumentation (which in the application of Beck’s theorem expresses ideas of fourth-order set theory and higher) is no doubt partly responsible for the somewhat fearsome reputation of topos theory.

In these notes I take a much less efficient but much more elementary approach, based on an arrangement of ideas which I hope can be seen as “natural” from the point of view of naive set theory. I learned of this approach from Myles Tierney, who was my PhD supervisor, and who with Bill Lawvere co-founded elementary topos theory, but I am not aware of any place where the details of this approach have been written up before now. I should also mention that the approach taken here is not as “purist” as many topos theorists might want; for example, here and there I take advantage of the strong extensionality axiom of ETCS to simplify some arguments.

The Empty Set and Two-Valued Logic

We begin with the easy observation that a terminal category, i.e., a category with just one object and one morphism (the identity), satisfies all the ETCS axioms. Ditto for any category equivalent to (where every object is terminal). Such boring ETCS categories are called degenerate; obviously our interest is in the structure of nondegenerate ETCS categories.

Let be an ETCS category (see here for the ETCS axioms). Objects of are generally called “sets”, and morphisms are generally called “functions” or “maps”.

Proposition 0: If an ETCS category is a preorder, then is degenerate.

Proof: Recall that a preorder is a category in which there is at most one morphism for any two objects . Every morphism in a preorder is vacuously monic. If there is a nonterminal set , then the monic to any terminal set defines a subset distinct from the subset defined by , thus giving (in an ETCS category) distinct classifying maps , contradicting the preorder assumption. Therefore all objects are terminal.

Assume from now on that is a nondegenerate ETCS category.

Proposition 1: There are at least two truth values, i.e., two elements , in .

Proof: By proposition 0, there exist sets and two distinct functions . By the axiom of strong extensionality, there exists such that . The equalizer of the pair is then a proper subset of , and therefore there are at least two distinct elements .

Proposition 2: There are at most two truth values ; equivalently, there are at most two subsets of .

Proof: If are distinct subsets of , then either or , say the former. Then and are distinct subsets, with distinct classifying maps . By strong extensionality, there exists distinguishing these classifying maps. Because is terminal, we then infer and , so as subsets of , and in that case only can be a proper subset of .

By propositions 1 and 2, there is a unique proper subset of the terminal object . Let denote this subset. Its domain may be called an “empty set”; by the preceding proposition, it has no proper subsets. The classifying map of is the truth value we call “false”.

Proposition 3: 0 is an initial object, i.e., for any there exists a unique function .

Proof: Uniqueness: if are maps, then their equalizer , which is monic, must be an isomorphism since 0 has no proper subsets. Therefore . Existence: there are monos

where is “global truth” (classifying the subset ) on and is the “singleton mapping ” on , defined as the classifying map of the diagonal map (last time we saw is monic). Take their pullback. The component of the pullback parallel to is a mono which again is an isomorphism, whence we get a map using the other component of the pullback.

Remark: For the “purists”, an alternative construction of the initial set 0 that avoids use of the strong extensionality axiom is to define the subset to be “the intersection all subsets of “. Formally, one takes the extension of the map

where the first arrow represents the class of all subsets of , and the second is the internal intersection operator defined at the end of our last post. Using formal properties of intersection developed later, this intersection has no proper subsets, and then the proof of proposition 3 carries over verbatim.

Corollary 1: For any , the set is initial.

Proof: By cartesian closure, maps are in bijection with maps of the form , and there is exactly one of these since 0 is initial.

Corollary 2: If there exists , then is initial.

Proof: The composite of followed by is , and followed by is also an identity since is initial by corollary 1. Hence is isomorphic to an initial object .

By corollary 2, for any object the arrow is vacuously monic, hence defines a subset.

Proposition 4: If , then there exists an element .

Proof: Under the assumption, has at least two distinct subsets: and . By strong extensionality, their classifying maps are distinguished by some element .

External Unions and Internal Joins

One of the major goals in this post is to construct finite coproducts in an ETCS category. As in ordinary set theory, we will construct these as disjoint unions. This means we need to discuss unions first; as should be expected by now, in ETCS unions are considered locally, i.e., we take unions of subsets of a given set. So, let be subsets.

To define the union , the idea is to take the intersection of all subsets containing and . That is, we apply the internal intersection operator (constructed last time),

to the element that represents the set of all subsets of containing and ; the resulting element represents . The element corresponds to the intersection of two subsets

Remark: Remember that in ETCS we are using generalized elements: really means a function over some domain , which in turn classifies a subset . On the other hand, the here is a subset . How then do we interpret the condition ““? We first pull back over to the domain ; that is, we form the composite , and consider the condition that this is bounded above by . (We will write , thinking of the left side as constant over .) Externally, in terms of subsets, this corresponds to the condition .

We need to construct the subsets . In ZFC, we could construct those subsets by applying the comprehension axiom scheme, but the axioms of ETCS have no such blanket axiom scheme. (In fact, as we said earlier, much of the work on “internalizing logic” goes to show that in ETCS, we instead derive a comprehension scheme!) However, one way of defining subsets in ETCS is by taking loci of equations; here, we express the condition , more pedantically or , as the equation

where the right side is the predicate “true over “.

Thus we construct the subset of via the pullback:

{C: A ≤ C} -------> 1
     |              |
     |              | t_X
     V chi_A => -   V
    PX -----------> PX

Let me take a moment to examine what this diagram means exactly. Last time we constructed an internal implication operator

and now, in the pullback diagram above, what we are implicitly doing is lifting this to an operator

The easy and cheap way of doing this is to remember the isomorphism we used last time to uncover the cartesian closed structure, and apply this to

to define . This map classifies a certain subset of , which I’ll just write down (leaving it as an exercise which involves just chasing the relevant definitions):

Remark: Similarly we can define a meet operator by exponentiating the internal meet . It is important to know that the general Heyting algebra identities which we established last time for lift to the corresponding identities for the operators on . Ultimately this rests on the fact that the functor , being a right adjoint, preserves products, and therefore preserves any algebraic identity which can be expressed as a commutative diagram of operations between such products.

Hence, for the fixed subset (classified by ), the operator

classifies the subset

Finally, in the pullback diagram above, we are pulling back the operator against . But, from last time, that was exactly the method we used to construct universal quantification. That is, given a subset

we defined to be the pullback of along . Putting all this together, the pullback diagram above expresses the definition

that one would expect “naively”.

Now that all the relevant constructions are in place, we show that is the join of and in the poset . There is nothing intrinsically difficult about this, but as we are still in the midst of constructing the internal logic, we will have to hunker down and prove some logic things normally taken for granted or zipped through without much thought. For example, the internal intersection operator was defined with the help of internal universal quantification, and we will need to establish some formal properties of that.

Here is a useful general principle for doing internal logic calculations. Let be the classifying map of a subset , and let be a function. Then the composite classifies the subset

so that one has the general identity . In passing back and forth between the external and internal viewpoints, the general principle is to try to render “complicated” functions into a form which one can more easily recognize. For lack of a better term, I’ll call this the “pullback principle”.

Lemma 1: Given a relation and a constant , there is an inclusion

as subsets of . (In traditional logical syntax, this says that for any element ,

implies

as predicates over elements . This is the type of thing that ordinarily “goes without saying”, but which we actually have to prove here!)

Proof: As we recalled above, was defined to be , the pullback of global truth along the classifying map . Hold that thought.

Let

be the map which classifies the subset . Equivalently, this is the map

under the canonical isomorphisms , . Intuitively, this maps , i.e., plugs an element into an element .

Using the adjunction of cartesian closure, the composite

transforms to the composite

so by the pullback principle, classifies .

Equivalently,

Also, as subsets of , we have the inclusion

[this just says that belongs to the subset classified by , or equivalently that is in the subset ]. Applying the pullback operation to (2), and comparing to (1), lemma 1 follows.

Lemma 2: If as subsets of , then .

Proof: From the last post, we have an adjunction:

if and only if

for any subset of . So it suffices to show . But

where the first inclusion follows from .

Next, recall from the last post that the internal intersection of was defined by interpreting the following formula on the right:

Lemma 3: If , then .

Proof: classifies the subset , i.e.,  is identified with the predicate in the argument , so by hypothesis as predicates on . Internal implication is contravariant in the argument [see the following remark], so

Now apply lemma 2 to complete the proof.

Remark: The contravariance of , that is, the fact that

implies

is a routine exercise using the adjunction [discussed last time]

if and only if

Indeed, we have

where the first inequality follows from the hypothesis , and the second follows from . By the adjunction, the inequality (*) implies .

Theorem 1: For subsets of , the subset is an upper bound of and , i.e., .

Proof: It suffices to prove that , since then we need only apply lemma 3 to the trivially true inclusion

to infer , and similarly . (Actually, we need only show . We’ll do that first, and then show full equality.)

The condition we want,

is, by the adjunction , equivalent to

which, by a – adjunction, is equivalent to

as subsets of . So we just have to prove (1). At this point we recall, from our earlier analysis, that

Using the adjunction , as in the proof of lemma 2, we have

which shows that the left side of (1) is contained in

where the last inclusion uses another – adjunction. Thus we have established (1) and therefore also the inclusion

Now we prove the opposite inclusion

that is to say

Here we just use lemma 1, applied to the particular element : we see that the left side of (**) is contained in

which collapses to , since . This completes the proof.

Theorem 2: is the least upper bound of , i.e., if is a subset containing both and , then .

Proof: We are required to show that

Again, we just apply lemma 1 to the particular element : the left-hand side of the claimed inclusion is contained in

but since is true by hypothesis (is globally true as a predicate on the implicit variable ), this last subset collapses to

which completes the proof.

Theorems 1 and 2 show that for any set , the external poset admits joins. One may go on to show (just on the basis of the topos axioms) that as in the case of meets, the global external operation of taking joins is natural in , so that by the Yoneda principle, it is classified by an internal join operation

namely, the map which classifies the union of the subsets

and this operation satisfies all the expected identities. In short, carries an internal Heyting algebra structure, as does for any set .

We will come back to this point later, when we show (as a consequence of strong extensionality) that is actually an internal Boolean algebra.

Construction of Coproducts

Next, we construct coproducts just as we do in ordinary set theory: as disjoint unions. Letting be sets (objects in an ETCS category), a disjoint union of and is a pair of monos

whose intersection is empty, and whose union or join in is all of . We will show that disjoint unions exist and are essentially unique, and that they satisfy the universal property for coproducts. We will use the notation for a disjoint union.

Theorem 3: A disjoint union of and exists.

Proof: It’s enough to embed disjointly into some set , since the union of the two monos in would then be the requisite . The idea now is that if a disjoint union or coproduct exists, then there’s a canonical isomorphism . Since the singleton map

is monic, one thus expects to be able to embed and disjointly into . Since we can easily work out how all this goes in ordinary naive set theory, we just write out the formulas and hope it works out in ETCS.

In detail, define to be

where is the singleton mapping and classifies ; similarly, define to be

Clearly and are monic, so to show disjointness we just have to show that their pullback is empty. But their pullback is isomorphic to the cartesian product of the pullbacks of the diagrams

so it would be enough to show that each (or just one) of these two pullbacks is empty, let’s say the first.

Suppose given a map which makes the square

  A -------> 1
  |          |
h |          | chi_0
  V sigma_X  V
  X -------> PX

commute. Using the pullback principle, the map classifies

which is just the empty subset. This must be the same subset as classified by (where is the diagonal), which by the pullback principle is

An elementary calculation shows this to be the equalizer of the pair of maps

So this equalizer is empty. But notice that equalizes this pair of maps. Therefore we have a map . By corollary 2 above, we infer . This applies to the case where is the pullback, so the pullback is empty, as was to be shown.

Theorem 4: Any two disjoint unions of are canonically isomorphic.

Proof: Suppose is a disjoint union. Define a map

where classifies the subset , and classifies the subset . Applying the pullback principle, the composite classifies

which is easily seen to be the diagonal on . Hence . On the other hand, classifies the subset

which is empty because and are disjoint embeddings, so . Similar calculations yield

Putting all this together, we conclude that and , where and were defined in the proof of theorem 3.

Next, we show that is monic. If not, then by strong extensionality, there exist distinct elements for which ; therefore, and . By the pullback principle, these equations say (respectively)

If , then both factor through the mono . However, since is monic, this would imply that , contradiction. Therefore . By similar reasoning, . Therefore

where is the negation operator. But then . And since is the union by assumption, must be the top element , whence is the bottom element 0. This contradicts the assumption that the topos is nondegenerate. Thus we have shown that must be monic.

The argument above shows that is an upper bound of and in . It follows that the join constructed in theorem 3 is contained in , and hence can be regarded as the join of and in . But is their join in by assumption of being a disjoint union, so the containment must be an equality. The proof is now complete.

Theorem 5: The inclusions , exhibit as the coproduct of and .

Proof: Let , be given functions. Then we have monos

Now the operation certainly preserves finite meets, and also preserves finite joins because it is left adjoint to . Therefore this operation preserves disjoint unions; we infer that the monos

exhibit as a disjoint union of . Composing the monos of (1) and (2), we have disjoint embeddings of and in . Using theorem 4, is isomorphic to the join of these embeddings; this means we have an inclusion

whose restriction to yields and whose restriction to yields . Hence extends and . It is the unique extension, for if there were two extensions , then the equalizer of and would be an upper bound of in , contradicting the fact that is the least upper bound. This completes the proof.

I think that’s enough for one day. I will continue to explore the categorical structure and logic of ETCS next time.

ETCS: Internalizing the logic

This post is a continuation of the discussion of “the elementary theory of the category of sets” [ETCS] which we had begun last time, here and in the comments which followed. My thanks go to all who commented, for some useful feedback and thought-provoking questions.

Today I’ll describe some of the set-theoretic operations and “internal logic” of ETCS. I have a feeling that some people are going to love this, and some are going to hate it. My main worry is that it will leave some readers bewildered or exasperated, thinking that category theory has an amazing ability to make easy things difficult.

• An aside: has anyone out there seen the book Mathematics Made Difficult? It’s probably out of print by now, but I recommend checking it out if you ever run into it — it’s a kind of extended in-joke which pokes fun at category theory and abstract methods generally. Some category theorists I know take a dim view of this book; I for my part found certain passages hilarious, in some cases making me laugh out loud for five minutes straight. There are category-theory-based books and articles out there which cry out for parody!

In an attempt to nip my concerns in the bud, let me remind my readers that there are major differences between the way that standard set theories like ZFC treat membership and the way ETCS treats membership, and that differences at such a fundamental level are bound to propagate throughout the theoretical development, and impart a somewhat different character or feel between the theories. The differences may be summarized as follows:

• Membership in ZFC is a global relation between objects of the same type (sets).
• Membership in ETCS is a local relation between objects of different types (“generalized” elements or functions, and sets).

Part of what we meant by “local” is that an element per se is always considered relative to a particular set to which it belongs; strictly speaking, as per the discussion last time, the same element is never considered as belonging to two different sets. That is, in ETCS, an (ordinary) element of a set is defined to be a morphism ; since the codomain is fixed, the same morphism cannot be an element of a different set . This implies in particular that in ETCS, there is no meaningful global intersection operation on sets, which in ZFC is defined by:

Instead, in ETCS, what we have is a local intersection operation on subsets of a set. But even the word “subset” requires care, because of how we are now treating membership. So let’s back up, and lay out some simple but fundamental definitions of terms as we are now using them.

Given two monomorphisms , we write ( if the monos are understood, or if we wish to emphasize this is local to ) if there is a morphism such that . Since is monic, there can be at most one such morphism ; since is monic, such must be monic as well. We say define the same subset if this is an isomorphism. So: subsets of are defined to be isomorphism classes of monomorphisms into . As a simple exercise, one may show that monos into define the same subset if and only if and . The (reflexive, transitive) relation on monomorphisms thus induces a reflexive, transitive, antisymmetric relation, i.e., a partial order on subsets of .

Taking some notational liberties, we write to indicate a subset of (as isomorphism class of monos). If is a generalized element, let us say is in a subset if it factors (evidently uniquely) through any representative mono , i.e., if there exists such that . Now the intersection of two subsets and is defined to be the subset defined by the pullback of any two representative monos . Following the “Yoneda principle”, it may equivalently be defined up to isomorphism by specifying its generalized elements:

Thus, intersection works essentially the same way as in ZFC, only it’s local to subsets of a given set.

While we’re at it, let’s reformulate the power set axiom in this language: it says simply that for each set there is a set and a subset , such that for any relation , there is a unique “classifying map” whereby, under , we have

The equality is an equality between subsets, and the inverse image on the right is defined by a pullback. In categorical set theory notation,

Hence, there are natural bijections

between subsets and classifying maps. The subset corresponding to is denoted or , and is called the extension of .

The set plays a particularly important role; it is called the “subset classifier” because subsets are in natural bijection with functions . [Cf. classifying spaces in the theory of fiber bundles.]

In ordinary set theory, the role of is played by the 2-element set . Here subsets are classified by their characteristic functions , defined by iff . We thus have ; the elementhood relation boils down to . Something similar happens in ETCS set theory:

Lemma 1: The domain of elementhood is terminal.

Proof: A map , that is, a map which is in , corresponds exactly to a subset which contains all of (i.e., the subobject ). Since the only such subset is , there is exactly one map .

Hence elementhood is given by an element . The power set axiom says that a subset is retrieved from its classifying map as the pullback .

Part of the power of, well, power sets is in a certain dialectic between external operations on subsets and internal operations on ; one can do some rather amazing things with this. The intuitive (and pre-axiomatic) point is that if has finite products, equalizers, and power objects, then is a representing object for the functor

which maps an object to the collection of subobjects of , and which maps a morphism (“function”) to the “inverse image” function , that sends a subset to the subset given by the pullback of the arrows , . By the Yoneda lemma, this representability means that external natural operations on the correspond to internal operations on the object . As we will see, one can play off the external and internal points of view against each other to build up a considerable amount of logical structure, enough for just about any mathematical purpose.

• Remark: A category satisfying just the first three axioms of ETCS, namely existence of finite products, equalizers, and power objects, is called an (elementary) topos. Most or perhaps all of this post will use just those axioms, so we are really doing some elementary topos theory. As I was just saying, we can build up a tremendous amount of logic internally within a topos, but there’s a catch: this logic will be in general intuitionistic. One gets classical logic (including law of the excluded middle) if one assumes strong extensionality [where we get the definition of a well-pointed topos]. Topos theory has a somewhat fearsome reputation, unfortunately; I’m hoping these notes will help alleviate some of the sting.

To continue this train of thought: by the Yoneda lemma, the representing isomorphism

is determined by a universal element , i.e., a subset of , namely the mono . In that sense, plays the role of a universal subset. The Yoneda lemma implies that external natural operations on general posets are completely determined by how they work on the universal subset.

Internal Meets

To illustrate these ideas, let us consider intersection. Externally, the intersection operation is a natural transformation

This corresponds to a natural transformation

which (by Yoneda) is given by a function . Working through the details, this function is obtained by putting and chasing

through the composite

Let’s analyze this bit by bit. The subset is given by

and the subset is given by

Hence is given by the pullback of the functions and , which is just

The map is thus defined to be the classifying map of .

To go from the internal meet back to the external intersection operation, let be two subsets, with classifying maps . By the definition of , we have that for all generalized elements

if and only if

(where the equality signs are interpreted with the help of equalizers). This holds true iff is in the subset and is in the subset , i.e., if and only if is in the subset . Thus is indeed the classifying map of . In other words, .

A by-product of the interplay between the internal and external is that the internal intersection operator

is the meet operator of an internal meet-semilattice structure on : it is commutative, associative, and idempotent (because that is true of external intersection). The identity element for is the element . In particular, carries an internal poset structure: given generalized elements , we may define

if and only if

and this defines a reflexive, symmetric, antisymmetric relation :

equivalently described as the equalizer

of the maps and . We have that if and only if .

Internal Implication

Here we begin to see some of the amazing power of the interplay between internal and external logical operations. We will prove that carries an internal Heyting algebra structure (ignoring joins for the time being).

Let’s recall the notion of Heyting algebra in ordinary naive set-theoretic terms: it’s a lattice that has a material implication operator such that, for all ,

if and only if

Now: by the universal property of , a putative implication operation is uniquely determined as the classifying map of its inverse image , whose collection of generalized elements is

Given , the equality here is equivalent to

(because is maximal), which in turn is equivalent to

This means we should define to be the classifying map of the subset

Theorem 1: admits internal implication.

Proof: We must check that for any three generalized elements , we have

if and only if

Passing to the external picture, let be the corresponding subsets of . Now: according to how we defined a generalized element is in if and only if . This applies in particular to any monomorphism that represents the subset .

Lemma 2: The composite

is the classifying map of the subset .

Proof: As subsets of , where the last equation holds because both sides are the subsets defined as the pullback of two representative monos , .

Continuing the proof of theorem 1, we see by lemma 2 that the condition corresponds externally to the condition

and this condition is equivalent to . Passing back to the internal picture, this is equivalent to , and the proof of theorem 1 is complete.

Cartesian Closed Structure

Next we address a comment made by “James”, that a category satisfying the ETCS axioms is cartesian closed. As everything else in this article, this uses only the fact that such a category is a topos: has finite products, equalizers, and “power sets”.

Proposition 1: If are “sets”, then represents an exponential

Proof: By the power set axiom, there is a bijection between maps into the power set and relations:

which is natural in . By the same token, there is a natural bijection

Putting these together, we have a natural isomorphism

and this representability means precisely that plays the role of an exponential .

Corollary 1: .

The universal element of this representation is an evaluation map , which is just the classifying map of the subset .

Thus, represents the set of all functions (that is, relations from to ). This is all we need to continue the discussion of internal logic in this post, but let’s also sketch how we get full cartesian closure. [Warning: for those who are not comfortable with categorical reasoning, this sketch could be rough going in places.]

As per our discussion, we want to internalize the set of such relations which are graphs of functions, i.e., maps where each is a singleton, in other words which factor as

where is the singleton mapping:

We see from this set-theoretic description that classifies the equality relation

which we can think of as either the equalizer of the pair of maps or, what is the same, the diagonal map .

Thus, we put , and it is not too hard to show that the singleton mapping is a monomorphism. As usual, we get this monomorphism as the pullback of along its classifying map .

Now: a right adjoint such as preserves all limits, and in particular pullbacks, so we ought then to have a pullback

       B^A ---------------> 1^A
        |                    |
sigma^A |                    | t^A
        V                    V
     P(B)^A -------------> P(1)^A
            (chi_sigma)^A

Of course, we don’t even have yet, but this should give us an idea: define , and in particular its domain , by taking the pullback of the right-hand map along the bottom map. In case there is doubt, the map on the bottom is defined Yoneda-wise, applying the isomorphism

to the element in the hom-set (on the left) given by the composite

The map on the right of the pullback is defined similarly. That this recipe really gives a construction of will be left as an exercise for the reader.

Universal Quantification

As further evidence of the power of the internal-external dialectic, we show how to internalize universal quantification.

As we are dealing here now with predicate logic, let’s begin by defining some terms as to be used in ETCS and topos theory:

• An ordinary predicate of type is a function . Alternatively, it is an ordinary element . It corresponds (naturally and bijectively) to a subset .
• A generalized predicate of type is a function . It may be identified with (corresponds naturally and bijectively to) a function , or to a subset .

We are trying to define an operator which will take a predicate of the form [conventionally written ] to a predicate [conventionally written ]. Externally, this corresponds to a natural operation which takes subsets of to subsets of . Internally, it corresponds to an operation of the form

This function is determined by the subset , defined elementwise by

Now, in ordinary logic, is true if and only if is true for all , or, in slightly different words, if is constantly true over all of :

The expression on the right (global truth over ) corresponds to a function , indeed a monomorphism since any function with domain is monic. Thus we are led to define the desired quantification operator as the classifying map of .

Let’s check how this works externally. Let be a generalized predicate of type . Then according to how has just been defined, classifies the subset

There is an interesting adjoint relationship between universal quantification and substitution (aka “pulling back”). By “substitution”, we mean that given any predicate on , we can always pull back to a predicate on (substituting in a dummy variable of type , forming e.g. ) by composing with the projection . In terms of subsets, substitution along is the natural external operation

Then, for any predicate , we have the adjoint relationship

if and only if

so that substitution along is left adjoint to universal quantification along . This is easy to check; I’ll leave that to the reader.

Internal Intersection Operators

Now we put all of the above together, to define an internal intersection operator

which intuitively takes an element (a family of subsets of ) to its intersection , as a subset .

Let’s first write out a logical formula which expresses intersection:

We have all the ingredients to deal with the logical formula on the right: we have an implication operator as part of the internal Heyting algebra structure on , and we have the quantification operator . The atomic expressions and refer to internal elementhood: means is in , and means is in .

There is a slight catch, in that the predicates “” and “” (as generalized predicates over , where lives) are taken over different domains. The first is of the form , and the second is of the form . No matter: we just substitute in some dummy variables. That is, we just pull these maps back to a common domain , forming the composites

and

Putting all this together, we form the composite

This composite directly expresses the definition of the internal predicate given above. By cartesian closure, this map induces the desired internal intersection operator, .

This construction provides an important bridge to getting the rest of the internal logic of ETCS. Since we can can construct the intersection of arbitrary definable families of subsets, the power sets are internal inf-lattices. But inf-lattices are sup-lattices as well; on this basis we will be able to construct the colimits (e.g., finite sums, coequalizers) that we need. Similarly, the intersection operators easily allow us to construct image factorizations: any function can be factored (in an essentially unique way) as an epi or surjection to the image, followed by a mono or injection . The trick is to define the image as the smallest subset of through which factors, by taking the intersection of all such subsets. Image factorization leads in turn to the construction of existential quantification.

As remarked above, the internal logic of a topos is generally intuitionistic (the law of excluded middle is not satisfied). But, if we add in the axiom of strong extensionality of ETCS, then we’re back to ordinary classical logic, where the law of excluded middle is satisfied, and where we just have the two truth values “true” and “false”. This means we will be able to reason in ETCS set theory just as we do in ordinary mathematics, taking just a bit of care with how we treat membership. The foregoing discussion gives indication that logical operations in categorical set theory work in ways familiar from naive set theory, and that basic set-theoretic constructions like intersection are well-grounded in ETCS.