Theory and Applications of Categories, Vol. 15, No. 5, 2005, pp. 147–163.

ALGEBRAIC MODELS OF INTUITIONISTIC THEORIES OF SETS AND CLASSES

S. AWODEY AND H. FORSSELL

Abstract. This paper constructs models of intuitionistic set theory in suitable categories. First, a Basic Intuitionistic Set Theory (BIST) is stated, and the categorical semantics are given. Second, we give a notion of an ideal over a category, using which one can build a model of BIST in which a given topos occurs as the sets. And third, a sheaf model is given of a Basic Intuitionistic Class Theory conservatively extending BIST. The paper extends the results in [2] by introducing a new and perhaps more natural notion of ideal, and in the class theory of part three.

1. Introduction

We begin with a very brief and informal sketch (elaborated in section 2 below) of the leading ideas of algebraic set theory, as it was recently presented in [2], and first proposed in [8] (see also [6, 7, 1]). The basic tool of algebraic set theory is the notion of a category with class structure, which provides an axiomatic framework in which models of set theory are constructed. Such a category C is equipped with three interrelated structures: a subcategory S ↪ C of small maps, a powerclass functor P : C [figure] C, and a universal class U in C. The small maps determine which classes are sets, the powerclass P(C) is the class of all subsets of a class C, and the universe U is a fixed point of P, in the sense that P(U) ≅ U (related conditions like P(U) ⊆ U are also considered).

The language of elementary set theory (first–order logic with a binary ‘membership’ relation ϵ) can be interpreted in any such universe U, and the elementary theory of all such universes can be completely axiomatized by a very natural system of set theory, called Basic Intuitionistic Set Theory (BIST), first formulated in [2]. It is noteworthy for including the unrestricted axiom scheme of Replacement in the absence of the full axiom scheme of Separation (a combination that can not occur in classical logic, where Replacement implies Separation).

The objects of a category with class structure that have a small morphism into the terminal object are called small objects or sets. These are easily shown to be a topos. In [2] it is shown that any topos whatsoever occurs as the subcategory of small objects in some category with class structure. This is achieved by defining a notion of an ideal on a topos. The main part of this paper consists in a modification of this notion (elaborated in section 3). It is shown that a useful notion of ideal on a topos can be obtained by considering certain sheaves on the topos under the coherent (or finite epimorphic families) covering. Namely, these are those sheaves that occur as colimits of filtered diagrams of representables, in which every morphism is a monomorphism. Following a suggestion by André Joyal, these sheaves are characterized as satisfying a “small diagonal” condition with respect to maps with representable fibers. The subcategory of such ideals then forms a category with class structure in which one can solve for fixed points of the powerobject functor.

Received by the editors 2005-01-12 and, in revised form, 2005-09-12.

Published on 2005-09-21 in the volume of articles from CT2004.

2000 Mathematics Subject Classification: 18B05, 18B25, 18C10, 03G30, 03E70, 03F60.

Key words and phrases: algebraic set theory, topos theory, sheaf theory.

\begin{matrix}c \\ ◯ \end{matrix} S. Awodey and H. Forssell, 2005. Permission to copy for private use granted.

If the powerclass of an ideal C is thought of as the class of all subsets of C, then the powerobject of C in the category of sheaves can be thought of as the “hyper class” of all subclasses of C, since ideals are closed under subsheaves. The first step in a comparison between these two kinds of powerobjects is carried out in section 4, where it is shown that there is a model in the category of sheaves of a Morse-Kelley style theory of sets and classes which is a conservative extension of BIST.

Acknowledgements. We have benefitted from collaboration and discussions with Carsten Butz, Alex Simpson, and Thomas Streicher. We have also had many helpful conversations with Ivar Rummelhoff, Dana Scott, and Michael Warren. Both André Joyal and Bill Lawvere made suggestions that lead to some of the results given here.

2. BIST and categories with class structure

2.1. Basic Intuitionistic Set Theory. We recall the following Basic Intuitionistic Set Theory—BIST— from [2]: The language has, in addition to the membership relation ϵ, a predicate S for “Sethood”. We make use of the shorthand notation of Sx. ϕ for ∃y. S(y) ∧ ∀x. (xϵy ↔ ϕ), where y is not free in ϕ. The expression x ⊆ y stands for S(x) ∧ S(y) ∧ ∀zϵx. zϵy.

BIST 1. (Membership) yϵx → S(x)

BIST 2. (Extensionality) x ⊆ y ∧ y ⊆ x → x = y

BIST 3. (Empty Set) Sz.⊥

BIST 4. (Pairing) Sz. z = x ∨ z = y

BIST 5. (Union) S(x) ∧ (∀yϵx. S(y)) → Sz. ∃yϵx. zϵy

BIST 6. (Replacement) S(x) ∧ (∀yϵx. ∃!z. ϕ) → Sz. ∃yϵx. ϕ

BIST 7. (Power Set) S(x) → Sy. y ⊆ x

BIST 8. (Intersection) S(x) ∧ (∀yϵx.y ⊆ w) → Sz. zϵw ∧ ∀yϵx.zϵy

These axioms allow us to define the usual notions of “ordered pair” and “function”, which allow us to state the last axiom of BIST, which we state informally as:

ALGEBRAIC MODELS OF INTUITIONISTIC THEORIES OF SETS AND CLASSES 149

BIST 9. (Infinity) There exists a set I with an injection s : I + 1 → I.

For the purposes of this paper, the axiom of Infinity is of no special interest. We introduce the notation !ϕ (read ‘ϕ is simple’) as a shorthand for:

Sz. z = ∅ ∧ ϕ

where z is not free in ϕ. Separation for simple formulas is provable in BIST [2]:

2.2. Proposition. (!-Separation)

BIST ⊢ (∀yϵx. !ϕ) → (S(x) → Sy. yϵx ∧ ϕ)

Certain closure conditions also hold for provably simple formulas [2]:

2.3. Lemma. In BIST, the following are provable:

1. !(x = y)

2. S(x) →!(yϵx)

3. !ϕ∧!ψ →!(ϕ ∧ ψ)∧!(ϕ ∨ ψ)∧!(ϕ → ψ)

4. S(x) ∧ ∀yϵx. !ϕ →!(∃yϵx. ϕ)∧!(∀yϵx. ϕ)

5. (ϕ ∨ ¬ϕ) →!ϕ

The following form of Δ_{0} separation therefore holds:

2.4. Definition. Given a Δ_{0} formula ϕ and a variable x in ϕ, we say that x is an orphan if x is free in ϕ. If x is not free, the we define the parent y of x to be the variable bounding x (i.e. such that ∀xϵy or ∃xϵy occurs in ϕ). Denote by F (ϕ, x) the (unique) tuple of variables ⟨y_{0}, y_{1}, …, y_{n}⟩ such that y_{0} = x, y_{m+1} is the parent of y_{m} for 0 ≤ m ≤ n, and y_{n} is an orphan. Next, we adopt the following abbreviation:

S(F (ϕ, x)) := S(y_{n}) ∧ ∀y_{n−1}ϵy_{n}.S(y_{n−1}) ∧ ∀y_{n−2}ϵy_{n−1}.S(y_{n−2}) ∧ … ∀xϵy_{1}. ∧ S(x)

2.5. Proposition. (Δ_{0}-Separation)

In BIST, separation holds for S–predicate free Δ_{0} formulas in the context of a “well– typing”, in the following sense: For a Δ_{0} formula ϕ in which the S–predicate does not occur, let x_{1}, …, x_{n}, be a list of all the variables occurring on the right hand side of an ϵ in ϕ. We have then that:

BIST ⊢ S(x) ∧ S(F (ϕ, x_{1})) ∧ … ∧ S(F (ϕ, x_{n})) → Syϵx. ϕ

We remark that in order to have unrestricted Δ_{0} separation, it is sufficient to add to BIST an axiom stating that the S–predicate is simple, !S(x).

2.6. Categories with class structure. Let C be a positive Heyting category, i.e. a Heyting category with finite disjoint coproducts that are stable under pullback (see [4, A1.4.4]). A system of small maps on C is a collection of morphisms of C satisfying the following conditions:

(S1) Every identity map Id_{A} : A  [figure] A is small, and the composite g ∘ f : A  [figure] C of
any two small maps f : A  [figure] B and g : B  [figure] C is again small.

(S2) The pullback of a small map along any map is small. Thus in an arbitrary pullback diagram,

[figure: C; D; A; C; f′; A; B; B; D; f]

f′ is small if f is small.

(S3) Every diagonal Δ : A [figure] A × A is small.

(S4) If f ∘ e is small and e is regular epic, then f is small, as indicated in the diagram:

[figure: A; C; e; A; B; f∘e; B; C; f]
(S5) Copairs of small maps are small. Thus if f : A  [figure] C and g : B  [figure] C are small,

then so is the copairing [f, g] : A + B [figure] C.

A relation r : R [figure] A × B is called a small relation if the second projection,

π_{2} ∘ r : R [figure] A × B [figure] B

is a small map. We make the small relations representable in requiring that C has (small) powerobjects consisting of, for every object A in C , an object P A and a small relation, ϵ_{A} [figure] A × P A, such that the following two axioms are satisfied:

(P1) For any small relation R [figure: m] A × B, there exists a unique classifying map,

ρ : B [figure] P A

such that the following is a pullback:

[figure: A × B; A × P A; Id×ρ; R; A × B; m; R; ϵ_{A}; ϵ_{A}; A × P A]

(P2) The internal subset relation ⊆_{A} [figure] P A × P A is a small relation (the definition of ⊆_{A} is as expected, see [2]).

For any morphism f : A [figure] B in C, the image of ϵ_{A} along f ×Id_{P A} is a small relation by S4. Its classifying map P f : P A [figure] P B, also known as the internal direct image map, is the morphism part of the powerobject functor P : C [figure] C.

A universal object U in C is an object such that for every object A in C, there exists a monomorphism A [figure] U. A universal object is in particular a universe, that is, an object U such that there exists a monomorphism P U [figure] U. We require the existence of a universal object:

(U) C has a universal object U.

A positive Heyting category C having a system of small maps satisfying S1-S5, powerobjects satisfying P1-P2, and a universal object we call a category with class structure, or briefly class category. We denote a category with this structure (C, S, P, U) or briefly C.

For a class category C, the universal object U together with a choice of inclusion ι : P U [figure] U gives us a structure for a first–order set theory (ϵ, S), by defining the interpretation [[x | S(x)]] to be the mono:

ι : P U [figure] U

and [[x, y | xϵy]] as the composite:

ϵ_{U} [figure] U × P U [figure] U × U

The following is proved in [2, Section 3]:

2.7. Theorem. The set theory BIST is sound and complete with respect to such models (U, ι) in class categories C:

BIST ⊢ ϕ iff, for all C, one has U ⊧_{C} ϕ

The completeness result is proved by defining a class structure on the first-order syntactic category of BIST. Briefly, a morphism [x, y | ϕ] : [x | ψ] [figure] [y | σ] is small if BIST ⊢_{y} Sx. ϕ; the powerobject of [x | ψ] is [u | S(u) ∧ ∀xϵu. ψ]; and U = [x | x = x].

3. Ideals over a topos

3.1. Small maps in sheaves. In a class category C, a small object is an object A such that the unique map A [figure] 1 is small. By [2], the small objects in C form a topos, and every topos occurs as the category of small objects in a category with class structure. The purpose of this section is to provide a new proof of the latter fact, using a more canonical construction that avoids some of the difficulties in the original proof.

Let a small topos (or, for this subsection, just a pretopos) E be given. Consider the category Sh(E) of sheaves on E, for the coherent covering [4, A2.1.11(b)]. Recall that the Yoneda embedding y : E ↪ Sh(E) is a full and faithful Heyting functor [4, D3.1.17].

We intend to build a class category in Sh(E) where the representables are the small objects. First, we define a system S of small maps on Sh(E) by including in S the morphisms of Sh(E) with “representable fibers” in the following sense:

3.2. Definition. [Small Map] A morphism f : A [figure] B in Sh(E) is small if for any morphism with representable domain g : yD [figure] B, there exists an object C in E, and morphisms f′, g′ in Sh(E) such that the following is a pullback:

[figure: A; B; f; yC; A; g′; yC; yD; f′; yD; B; g]

Thus, in this sense, small maps pull representables back to representables.

3.3. Proposition. S satisfies axioms S1, S2, and S5.

Proof. S1 and S2 follow easily from the Two Pullback lemma.

For S5, the pullback of, say, yD [figure: h] C along [f, g] : A + B [figure] C is the coproduct of the pullback of h along f and of h along g. But this is representable, since representables are closed under finite coproducts in Sh(E).

We move to consider S3. A directed diagram (in a category C, say) is a functor I [figure] C where I is a directed preorder. A small directed diagram in C in which (the image of) every morphism is a monomorphism in C we shall call an ideal diagram. An ideal diagram has no non-trivial parallel pairs, and is therefore also a filtered diagram.

3.4. Definition. [Ideal over E] An object A in Sets^{E^{op}} is an ideal over E if it can be written as a colimit of an ideal diagram I [figure] E of representables,

A ≅ \underrightarrow{Lim}_{I}(yC_{i})

3.5. Lemma. Every ideal is a sheaf.

Proof. Since an ideal diagram is a filtered diagram, filtered colimits commute with finite limits, being a sheaf is a finite limit condition, and all representables are sheaves, all such presheaves are also sheaves.

In accordance with a conjecture by André Joyal, it now turns out that the ideals over E are exactly the sheaves for which S3 holds, i.e. for which the diagonal A [figure] A × A is small:

3.6. Lemma. Any sheaf F can be written as a colimit (in Sets^{E^{op}}) of representables \underrightarrow{Lim}_{I}(yC_{i}) where I has the property that for any two objects i, j in I, there is an object k

in I and morphisms i  [figure] k and j  [figure] k (i.e. I is directed).

Proof. We may write a sheaf F as the colimit of the composite functor,

∫ F [figure: π] E [figure: y] Sets^{E^{op}}

where ∫ F is the category of elements of F, and π is the forgetful functor. The objects in Sh(E) can be characterized as the functors E^{op} [figure] Sets which preserve monomorphisms and finite products. It follows that ∫ F has the required property, since for any two objects (A, a), (B, b) in ∫ F (with a ∈ F A, b ∈ F B),

[figure: (A, a); (A + B, ⟨a, b⟩); (A + B, ⟨a, b⟩); (B, b)]

(By the coproduct A + B, we mean the coproduct in E, hence the product A × B in E^{op}, which is sent to the product F A × F B in Sets.)

3.7. Theorem. For any sheaf F, the following are equivalent:

1. F is an ideal.

2. The diagonal F [figure] F × F is a small map.

3. For all arrows with representable domain f : yC [figure] F, the image of f in sheaves is representable, f : yC [figure] yD [figure] F, for some D in E.

Proof. (1)⇒(2):

We write F as an ideal diagram of representables, F = \underrightarrow{Lim}_{I}(yC_{i}). Note that the

pullback of any arrow A [figure: f] F × F along F [figure: Δ] F × F is the equalizer of the pair

A [figure: π_{1}f; π_{2}f] F.

Thus let g, h : yD [figure] F be given, and we must verify that their equalizer e : E [figure] yD is representable. Recall that, in Sets^{E^{op}}, if we are given a colimit \underrightarrow{Lim}_{I}(yC_{i}) and an arrow

[figure: yX; \underrightarrow{Lim}_{I}(yC_{i}); f] , then f factors through the base of the colimiting cocone, i.e. there is an e : X [figure] C_{i} such that,

[figure: yX; \underrightarrow{Lim}_{I}(yC_{i}); f; yX; yC_{i}; e; yC_{i}; \underrightarrow{Lim}_{I}(yC_{i}); f_{i}]

for some i (where f_{i} is an arrow of the colimiting cocone). Hence we may factor h as

yX [figure: e_{h}] yC_{i} [figure: f_{i}] \underrightarrow{Lim}_{I}(yC_{i}) and g as yX [figure: e_{g}] C_{j} [figure: f_{j}] \underrightarrow{Lim}_{I}(yC_{i}). Since the diagram is directed, there is a C_{k} and arrows u, v such that the two triangles in the following commute:

[figure: yC_{j}; yC_{k}; v; yD; yC_{j}; e_{g}; yD; yC_{i}; e_{h}; yC_{i}; yC_{k}; u; yC_{i}; F; f_{i}; yC_{k}; F; f_{k}; yC_{j}; F; f_{j}]

Since f_{k} is monic, the equalizer e : E [figure] yD of h = f_{k}ue_{h} and g = f_{k}ve_{g} is precisely the equalizer of ue_{h} and ve_{g}. But Yoneda preserves and reflects equalizers, so we may conclude that the equalizer of h and g is representable, E ≅ yC.

(2)⇒(3):

Let yD [figure: f] F be given. The kernel pair k_{1}, k_{2} of f can be described as the pullback:

[figure: yD × yD; F × F; f×f; K; yD × yD; (k_{1},k_{2}); K; F; F; F × F; Δ]

Since yD × yD ≅ y(D × D) is representable and the diagonal of F is small, K is representable (K ≅ yK, with some abuse of notation). Hence we may rewrite the kernel pair as

yK [figure: yk_{1}; yk_{2}] yD [figure: f] F

The kernel pair is an equivalence relation in Ê. Since Yoneda is full and faithful and

cartesian, K [figure: k_{1}; k_{2}] D is an equivalence relation in E. Since E is effective, there is a

coequalizer

K [figure: k_{1}; k_{2}] D [figure: e] E

such that k_{1} and k_{2} is the kernel pair of e. Since Yoneda preserves pullbacks and regular epis into Sh(E),

yK [figure: yk_{1}; yk_{2}] yD [figure: ye] yE

is a coequalizer diagram in Sh(C). This gives us, then, the required epi–mono factorization:

[figure: yD; yE; ye; yD; F; f; F; yE; yK; yD; yk_{1}; yK; yD; yk_{2}]

(3)⇒(1):

Step 1: To construct an ideal diagram of representables.

We write F as a colimit F = \underrightarrow{Lim}_{I}(yD_{i}), in accordance with Lemma 3.6 (so that I is the category of elements of F). Now, for each i ∈ I, factor in sheaves the cocone arrow

yD_{i} [figure: f_{i}] F:

[figure: yD_{i}; yE_{i}; ye_{i}; yD_{i}; F; f; F; yE_{i}; m_{i}]

For yD_{i} [figure: u] yD_{j} in the diagram I, consider the diagram:

[figure: yD_{j}; yE_{j}; ye_{j}; yD_{i}; yD_{j}; u; yD_{i}; yE_{i}; ye_{i}; yE_{i}; yE_{j}; v; F; yE_{j}; m_{j}; yE_{i}; F; m_{i}; yE_{i}; yE_{j}]

Since f_{i} = f_{j}u, it follows that f_{i} factors through yE_{j}, which gives us the mono v, making the triangle in the diagram commute (to see this, the diagram must be considered in Sh(E), where e_{i} is a cover). Since m_{j} is monic, the square commutes.

The new diagram I′ of the yE_{i} and v thus obtained is directed, since I has the property described in Lemma 3.6 and any parallel pair of arrows collapse by the construction.

Step 2: To show F ≅ \underrightarrow{Lim}_{I′}(yE_{i})

Observe that the ye_{i}’s in the diagram above give us a morphism e : \underrightarrow{Lim}_{I}yD_{i} [figure] \underrightarrow{Lim}_{I′}yE_{i}, while the m_{i}’s give us a monomorphism \underrightarrow{Lim}_{I′}yE_{i} [figure] F, such that the following commutes:

[figure: \underrightarrow{Lim}_{I}yD_{i}; F; ≅; \underrightarrow{Lim}_{I}yD_{i}; \underrightarrow{Lim}_{I′}yE_{i}; e; \underrightarrow{Lim}_{I′}yE_{i}; F; m]

Thus m is also an isomorphism.

In order to ensure that S3 is satisfied, we therefore narrow our attention from Sh(E) to the full subcategory of ideals, denoted Idl(E). We shall see that no further restriction is needed. First, we verify that Idl(E) is a positive Heyting category:

3.8. Lemma. Idl(E) is closed under subobjects and finite limits.

Proof. We use the description of ideals as sheaves with small diagonal. That Idl(E) is closed under subobjects follows from S2.

1 [figure: Δ] 1 × 1 is iso, hence small.

If A, B are ideals and C is any sheaf, we consider the pullback:

[figure: A; C; f; D; A; k_{1}; D; B; k_{2}; B; C; g]

Now, if we pull the diagonals back:

[figure: D × D; A × A; k_{1}×k_{1}; A_{1}; D × D; α; A_{1}; A; A; A × A; Δ; D × D; B × B; k_{2}×k_{2}; B_{1}; D × D; β; B_{1}; B; B; B × B; Δ]

By a diagram chase, the diagonal of D is A_{1} ∩ B_{1}, which is small since smallness is preserved by pullback and composition.

3.9. Lemma. Idl(E) is closed under finite coproducts (of sheaves), and inclusion maps are small.

Proof. 0 [figure] 0 × 0 is iso, so small.

Now, the terminal object 1 in Sh(E) is representable, and so is 1 + 1, since Yoneda preserves finite coproducts. The inclusion i_{1} : 1 [figure] 1+1 is therefore small. But coproducts in Sh(E) being disjoint, the following is a pullback:

[figure: A + B; 1 + 1; !_{A}+!_{B}; A; A + B; i_{A}; A; 1; 1; 1 + 1; i_{1}]

So by S2, the inclusion map i_{A} is small.

The diagonal of A + B can be regarded as the disjoint union of the diagonal of A and of B:

By smallness of coproduct inclusions and isos, and applying S5, if A, B are ideals then so is A + B.

[figure: A × A; (A + B) × (A + B); A; A × A; Δ; A; A + B; p_{A}; A + B; (A + B) × (A + B); Δ; (A + B) × (A + B); B × B; A + B; (A + B) × (A + B); A + B; B; p_{B}; B; B × B; Δ; A × A; (A + B) × (A + B); A × A; (A × A) + (A × B) + (B × A) + (B × B); p_{A×A}; (A + B) × (A + B); (A × A) + (A × B) + (B × A) + (B × B); (A + B) × (A + B); B × B; (A + B) × (A + B); (A × A) + (A × B) + (B × A) + (B × B); ≅; B × B; (A × A) + (A × B) + (B × A) + (B × B); p_{B×B}]

3.10. Proposition. Idl(E) is positive Heyting, and this structure can be calculated in Sh(E).

Proof. We have done finite limits and finite coproducts. For a morphism f : A [figure] B of ideals, Im(f) is an ideal, since there is a monomorphism Im(f) [figure] B. The cover e : A [figure] Im(f) is the coequalizer of its kernel pair in Sh(E), the kernel pair is the same in Idl(E), so e is also a regular epimorphism in Idl(E).

For dual images, since Idl(E) is closed under subobjects and finite limits can be taken in sheaves, dual images can also be taken in sheaves.

3.11. Lemma. S4 is satisfied in Idl(E).

Proof. Let A [figure: a] B [figure: b] C be given, and assume b ∘ a is small. Let yG [figure] C be given, and consider the following two pullback diagram:

[figure: A; B; a; yD; A; yD; E; E; B; B; C; b; E; B; E; yG; yG; C]

By Theorem 3.7, the image of a representable is a representable in Idl(E). Hence E in the diagram above is (isomorphic to) a representable.

We summarize the results of this subsection:

3.12. Theorem. For any pretopos E, the full subcategory Idl(E) ↪ Sh(E) of ideals is a positive Heyting category with a system of small maps satisfying axioms S1–S5.

3.13. Powerobjects and universes in Idl(E). We end the section with a brief discussion of the remaining part of the class structure in Idl(E), powerobjects and universes. In this subsection, we require E to be a topos, for we shall use the powerobjects in E to build powerobjects for ideals. Here we rely heavily on the characterization of Idl(E) as the colimits of ideal diagrams of representables. As such, Idl(E) is a subcategory of Ind(E), the category of filtered colimits of representables. We refer to [4, section C2] for the properties of Ind(E). Much of what is said about Idl(E) here are just special cases of that.

3.14. Lemma. Idl(E) has colimits of ideal diagrams (“ ideal colimits”).

Proof. Any such diagram is an ideal diagram of representables, see [4, section C2].

3.15. Proposition. If C is a category with ideal colimits, and F : E [figure] C is a functor which preserves monomorphisms, then there is a unique (up to natural isomorphism) extension F̃ : Idl(E) [figure] C of F such that F̃ is continuous, in the sense of preserving ideal colimits, and such that the following commutes:

[figure: Idl(E); C; F̃; Idl(E); E; y; C; E; F]

Proof. Write E = \underrightarrow{Lim}_{I}(yC_{i}) and set F̃(E) = \underrightarrow{Lim}_{I}(F C_{i}).

The powerobject functor P : E  [figure] E preserves monomorphisms, as does y : E  [figure] Idl(E),

and so y ∘ P extends to a continuous functor P : Idl(E) [figure]Idl(E). If \underrightarrow{Lim}_{I}(yA_{i}) is an ideal then \underrightarrow{Lim}_{I}(yP A_{i}) is its powerobject. The epsilon subobject is similarly constructed.

3.16. Proposition. With these powerobjects, Idl(E) satisfies P1 and P2.

Proof. We do one example: Let yC be a small subobject of the ideal \underrightarrow{Lim}_{I}(yA_{i}). The inclusion arrow yC [figure] \underrightarrow{Lim}_{I}(yA_{i}) factors through some yA_{i}, and we get the following diagram:

[figure: \underrightarrow{Lim}_{I}(yA_{i}) × 1; \underrightarrow{Lim}_{I}(yA_{i}) × \underrightarrow{Lim}_{I}(yP A_{i}); yA_{i} × 1; \underrightarrow{Lim}_{I}(yA_{i}) × 1; yA_{i} × 1; yA_{i} × yP A_{i}; Id×α; yA_{i} × yP A_{i}; \underrightarrow{Lim}_{I}(yA_{i}) × \underrightarrow{Lim}_{I}(yP A_{i}); yA_{i} × 1; yA_{i} × yP A_{i}; yC; yA_{i} × 1; yC; yϵ_{A_{i}}; yϵ_{A_{i}}; yA_{i} × yP A_{i}]

whence we get the global point 1 [figure] \underrightarrow{Lim}_{I}(yP A_{i}) classifying yC.

The main point is that every small subobject B [figure] \underrightarrow{Lim}_{I}(yA_{i}) of an ideal is already a (small) subobject B [figure] yA_{i} of some yA_{i} in the diagram.

Since the powerobject functor P is continuous in the above sense, we can find fixed points for it. For one example, we compose P on Idl(E) with the continuous functor C ↦ A + C for a fixed A in Idl(E). To construct a universal object, we wish for every representable to have a monomorphism into our universe, so take as our starting point A := ∐_{C∈E} yC (where the coproduct is taken in sheaves). This is an ideal, for it is the colimit of the ideal diagram of finite coproducts of representables, which themselves are representable, with arrows the coproduct inclusions.

Now consider the diagram

A [figure: i_{A}] A + P A [figure: Id_{A}+P i_{A}] A + P (A + P A) [figure]…

Call the colimit U. Then A + P U [figure: ≅] U, so we have a universe consisting of the class A of atoms and the class P U of sets. (U is the free algebra on A for the endofunctor P.)

Although it is a universe, U is not yet a universal object. We obtain, finally, our category with class structure containing E as the small objects by cutting out the part of Idl(E) we need (as in [7]):

3.17. Proposition. If (C, S, P) is a category with class structure (with or without a universal object) and U is a universe in C, then the full subcategory ↓ (U) of objects A in C such that there exists a monomorphism A [figure] U is a category with class structure, with the structure it inherits from C, and with U as its universal object.

Proof. We can demonstrate the existence of a encoded ordered pair map U ×U [figure] P P U which, when composed with the inclusions P P U [figure] P U [figure] U gives a monomorphism U × U [figure] U. The rest is straightforward (see also [7]).

There are of course a number of universes in Idl(E) that contain the representables, in the sense above. From [2], we know that:

3.18. Theorem. BIST+Coll is sound and complete with respect to class categories of the form ↓(U) [figure]Idl(E), for toposes E and universes U containing the representables.

Here, we either do not consider BIST to include an axiom of infinity, or we restrict attention to topoi containing a natural numbers object, see [2] and [3] for details. Coll is the axiom scheme of Collection which says that for any total relation R from a set A to the universe, there is a set B contained in the range of R such that the restriction of R to A × B is total on A and B:

(Coll) S(z) ∧ (∀xϵz. ∃y. ϕ) → ∃w. (S(w) ∧ (∀xϵz. ∃yϵw. ϕ) ∧ (∀yϵw. ∃xϵz. ϕ))

This condition is equivalent to requiring that the powerset functor P : C [figure] C preserves regular epimorphisms.

4. BICT and full powerobjects

4.1. BICT. We introduce the following Basic Intuitionistic Class Theory:^{1} Its language is a two-typed first-order language, where we use lower case variables for the “type of elements” and upper case variables for the “type of classes”. There is a “Sethood” predicate S and a binary “element” relation ϵ, both of which are “element”-typed. In addition, there is a binary predicate η which takes elements on the left and classes on the right:

BICT1. (BIST axioms)

All axioms of BIST, i.e. BIST1–BIST9, except, if one prefers, Replacement, which gets covered below.

BICT2. (Class extensionality)

(∀z. zηX ↔ zηY) → X = Y

BICT3. (Replacement) For any formula ϕ:

S(x) ∧ (∀yϵx. ∃!z. ϕ) → Sz. ∃yϵx. ϕ

BICT4. (Comprehension) For any formula ϕ (X not free in ϕ):

∃X. ∀z. zηX ↔ ϕ

1The axiomatization of BICT with respect to BIST is based on the axiomatization of Morse–Kelley with respect to ZF, as this axiomatization is presented in [5].

We say that a class is represented by a set if they have the same elements. Replacement now holds also for formulas ϕ with class quantifiers. Actually, it need not be a schema, since one could reformulate it as: If the domain of a functional class of ordered pairs is represented by a set, then so is the image.

4.2. A model of BICT in sheaves. Let two categories and a functor z : C ↪ G be given, and assume that

• C is a category of classes.

• G is a topos.

• z is full and faithful and Heyting.

• zC generates G (in the sense that if f ≠ g : G [figure] G′ in G then there is some h : zC [figure] G such that fh ≠ gh.)

Then we shall conclude that G contains a model of BICT.

4.3. Lemma. If C ∈ C, then C/C and G/zC and z/C : C/C [figure] G/zC inherit the above-listed properties.

Proof. The class structure is preserved by slicing by [2].

Denote by U the universal object of C, and consider the relation zϵ_{U} [figure] zU × zP U. Then there exists a unique classifying arrow κ : zP U [figure] P zU making the following a pullback in G:

[figure: zU × zP U; zU × P zU; Id×κ; zϵ_{U}; zU × zP U; zϵ_{U}; ϵ_{zU}; ϵ_{zU}; zU × P zU]

where (P zU, ϵ_{zU}) is the (full) powerobject in the topos G. We claim that the objects zU and P zU model BICT, with [[x | S(x)]] interpreted as zP U [figure: zι] zU, [[x, y | xϵy]] as the

composite zϵ_{U} [figure] zU × zP U [figure: Id×zι] zU × zU, and [[x, Y | xηY]] as ϵ_{zU} [figure] zU × P zU. Let us call this structure M.

Because the standard notation for class categories is so similar to the notation usually employed for topoi, we introduce some modifications. We shall often not bother to write out the z denoting the embedding. Instead, we write P_{s}A for the powerobject of A in C, and call it the small powerobject of A. ϵ_{A} remains the notation for the (small) elementhood relation in C. We continue to use P A for the powerobject in G (or P zA, if it is not clear from context that A is in the image of z), but we denote the full elementhood relation by η_{A}. Our pullback diagram above will then look like this:

[figure: U × P_{s}U; U × P U; Id×κ; ϵ_{U}; U × P_{s}U; ϵ_{U}; η_{U}; η_{U}; U × P U]

4.4. Proposition. M models BICT.

Proof.

BICT1 (BIST axioms): Since z is Heyting.

BICT2 (Class extensionality): By topos extensionality.

BICT3 (Replacement): The proof in [2] that replacement (BIST6) holds in a category with class structure carries over to our case, using Lemma 4.3 and the fullness of z and the fact that zC generates G. Briefly, the idea is that it is sufficient (thanks to Lemma 4.3) to consider the case where ϕ defines a functional relation between a small subobject of U and U. Thus ϕ defines a morphism between two objects in the image of z. z being full, this morphism is itself in the image of z. Since z is Heyting, we can carry out the image factorization in C to obtain, using axiom S4, that the image must be a small object.

BICT4 (Comprehension): By topos comprehension.

4.5. Corollary. BICT is a conservative extension of BIST.

Proof. Let C be the syntactic category of BIST, G the category of sheaves (coherent covering) on C and z the Yoneda embedding.

Another instance worth considering is when C is ↓(U) in Idl(E) for some topos E, and G is the category of sheaves on E (coherent covering), and z is the embedding of ↓ (U) into Sh(E). This gives a model of BICT in which the arbitrary topos E occurs as the sets.

We end this paper with some further observations concerning the case where C is a syntactic category. Observe that BIST may be extended to many a familiar set theory by adding appropriate axioms. The syntactic category of this set theory is still a class category, and the model M in sheaves is then a model of BICT extended by the axioms originally added to BIST.

For instance, BIST may be extended to ZF by adding an axiom of universal sethood stating that every thing is a set, an axiom of foundation, and the law of excluded middle (LEM) for every formula of the language. Adding these axioms to BICT, then, preserves conservativity. Call the theory consisting of BICT and these new axioms BIMK (Basic Intuitionistic Morse–Kelley). Note that we have added LEM only for formulas of BIST, i.e. those without class variables.

4.6. Corollary. BIMK is a conservative extension of ZF.

Separation—the assertion that the intersection of a class with a represented class yields a represented class—fails in general in BICT and in BIMK (and as a result, these extensions may at first strike the reader as rather pointless). However, we may repeat the analysis of simplicity from BIST to yield the following:

4.7. Lemma.

BICT ⊢ (S(x) ∧ ∀yϵx. Sz. z = ∅ ∧ yηX) → Sy. yϵx ∧ yηX

Proof. As in BIST.

Finally, we introduce a predicate !X for ∀x.!(xηX), to be read “X is simple”. Observe that in BIMK, !X iff ∀x.(xηX∨¬(xηX)), and the simple classes are just the complemented ones. The subobject [[X | !X]] [figure] P U is of independent interest, as it is the exponent (P_{s}1)^{U}. We will not go into the analysis of these objects here, but simply point out that if we use these objects, instead of the sheaf powerobjects, as our “types of classes”, we will get a class theory with full separation but restricted comprehension, instead of full comprehension and restricted separation. In the case where C is the syntactic category of ZF and G is the category of sheaves on C, it can be shown that we have comprehension for any formula ϕ in which every class variable is free. We state the implication of this for BIMK, but leave the proof for a proper presentation of simplicity, in BIST and BICT, and the simple powerobjects (P_{s}1)^{A}.

4.8. Proposition. Let M be the model of BIMKin sheaves on the syntactic category of ZF. If a formula ϕ in BIMK is such that all class variables X, Y, …, Z occurring in ϕ are free, then

M ⊧!X∧!Y ∧ … ∧!Z → (∀x. ∃y. ∀z. zϵy ↔ zϵx ∧ ϕ)

(where x and y are not free in ϕ).

References

[1] I. Rummelhoff, Class categories and polymorphic Π_{1} types. PhD thesis, University of Oslo, forthcoming.

[2] S. Awodey, C. Butz, A. Simpson, and T. Streicher, Relating topos theory and set theory via categories of classes. Tech. Report CMU-PHIL-146, Carnegie Mellon, 2003. Available from:

      www.phil.cmu.edu/projects/ast

[3] P. Aczel and M. Rathjen, Notes on Constructive Set Theory. Technical Report 40, Institut Mittag-Leffler (Royal Swedish Academy of Sciences), 2001.

[4] P. T. Johnstone, Sketches of an Elephant. Clarendon Press, Oxford, 2002.

[5] A. A. Fraenkel and Y. Bar–Hillel, Foundations of Set Theory, 1st edition. North–Holland Publishing Company, Amsterdam, 1958.

[6] C. Butz, Gödel-Bernays type theory. Journal of Pure and Applied Algebra, 178(1):1–23, 2003.

[7] A. Simpson, Elementary Axioms for Categories of Classes (Extended Abstract). In Fourteenth Annual IEEE Symposium on Logic in Computer Science: 77–85, 1999.

[8] A. Joyal and I. Moerdijk, Algebraic set theory. London Mathematical Society, Lecture Note Series 220, Cambridge University Press, 1995.

Carnegie Mellon University, Pittsburgh, PA

Email: awodey@cmu.edu
      jforssel@andrew.cmu.edu

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/15/5/15-05.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX 2ε is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@mathstat.uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca