Theory and Applications of Categories, Vol. 15, No. 1, 2005, pp. 1–39.

PREDICATIVE ALGEBRAIC SET THEORY

STEVE AWODEY AND MICHAEL A. WARREN

Abstract. In this paper the machinery and results developed in [Awodey et al, 2004] are extended to the study of constructive set theories. Specifically, we introduce two constructive set theories BCST and CST and prove that they are sound and complete with respect to models in categories with certain structure. Specifically, basic categories of classes and categories of classes are axiomatized and shown to provide models of the aforementioned set theories. Finally, models of these theories are constructed in the category of ideals.

The purpose of this paper is to generalize the machinery and results developed by Awodey, Butz, Simpson and Streicher in [Awodey et al, 2004] to the predicative case. Specifically, in ibid. it was shown that:

1. every category of classes contains a model of the intuitionistic, elementary set theory BIST,

2. BIST is logically complete with respect to such class category models,

3. the category of sets in such a model is an elementary topos,

4. every topos occurs as the sets in such a category of classes.

It follows, in particular, that BIST is sound and complete with respect to topoi as they can occur in categories of classes.^{1} Thus, in a very precise sense, BIST represents exactly the elementary set theory whose models are the elementary topoi.

In the current paper, we show that the same situation obtains with respect to a weaker, predicative, set theory CST which lacks the powerset axiom, and the new notion of a predicative topos (called a Π-pretopos, and defined as a locally cartesian closed pretopos).^{2} As in the impredicative case, the correspondence between the set theory and the category is mediated by a suitable category of classes, now weakened by the omission of the small

We wish to acknowledge many helpful discussions with Carsten Butz, Henrik Forssell, Nicola Gambino, André Joyal, Ivar Rummelhoff, Dana Scott, Thomas Streicher, and especially Alex Simpson.

Received by the editors 2004-12-27. Published on 2005-04-12 in the volume of articles from CT2004. 2000 Mathematics Subject Classification: 18B05, 18B25, 18C10, 03G30, 03E70, 03F60. Key words and phrases: algebraic set theory, categorical logic, predicativity, ideal completion, de-

pendent type theory, Π-pretopos, small maps.

\begin{matrix}c \\ ◯ \end{matrix} Steve Awodey and Michael A. Warren, 2005. Permission to copy for private use granted. 1It was also shown that every category of classes embeds into one of a special kind (the “ideal comple-

tion” of a topos), strengthening the completeness statement to topoi occurring in this special way. The predicative analogue of that result will not be considered here.

2A better notion of predicative topos is a Π-pretopos with W-types (cf. [Moerdijk and Palmgren, 2000] and [Moerdijk and Palmgren, 2002]). However, such categories will not be considered in this paper.

powerset condition (P2). This condition essentially asserted that the powerobject P_{s} (A) of a small object A is again small; in its place, we adopt the requirement that the exponential B^{A} of small objects A and B is again small. We also consider an even weaker, basic set theory BCST without the exponentiation axiom, for which the corresponding categories of sets are exactly the Heyting pretopoi.

The categories of sets at issue are briefly introduced in section 1 below, and the elementary set theories in section 2. Section 3 then develops the predicative categories of classes and shows that the set theories are indeed sound and complete for such class category models. This development follows that of [Awodey et al, 2004] quite closely, and it displays just how flexible and powerful the method developed there proves to be. To establish point (4) above in ibid., the notion of an ideal in a topos was invented and exploited. This concept has turned out to be quite robust and important. We here follow a suggestion of Joyal’s to reformulate it as a certain diagonal condition on sheaves.^{3} As such, it also becomes a very flexible tool for the construction of class categories of various kinds.

The main technical result in these paper is Proposition 4.21, stating that for any Heyting pretopos E, the small powerobject P_{s} (A) of an ideal A on E is again an ideal; this is key for the possibility of constructing a predicative category of classes with E as its category of sets. The construction makes use of the fact that the category of ideals over any pretopos E already satisfies the axioms for small maps as was shown in [Awodey and Forssell, 2004]. These topics are presented in section 4.

Taken together, these results show that CST is exactly the elementary set theory of Π-pretopoi, while BCST is the set theory of Heyting pretopoi. Indeed, syntactic versions of these facts, involving translations of theories, can even be given, although we do not pursue that here (cf. [Rummelhoff, 2004]).

Recently Gambino [Gambino, 2004] has studied presheaf models of constructive set theories. One interesting aspect of this work is that it serves to relate the approach of Joyal and Moerdijk with that of Scott [Scott, 1985]. However, we will not have occasion to discuss these results in this paper.

Finally, a fuller treatment of all of the results contained in this paper may be found in the second author’s Master’s thesis [Warren, 2004].

1. Π–Pretopoi

A locally cartesian closed category C is a cartesian category such that each slice C/D is cartesian closed. We will be interested in those locally cartesian categories which possess additional structure; namely, those which are also pretopoi. As such we adopt the following definition.

1.1. Definition. A Π-pretopos is a locally cartesian closed pretopos.

3See [Awodey and Forssell, 2004] for a fuller treatment.

Although we will not be particularly concerned with studying the properties of Πpretopoi the following fact should be noted.

1.2. Proposition. Every Π-pretopos R is Heyting.

The reader should recall the following theorem which affirms a tight connection between locally cartesian closed categories and dependent type theory (cf. [Johnstone, 2003] or [Jacobs, 1999]):

1.3. Theorem. [LCCC Soundness and Completeness] For any judgement in context Γ|φ of dependent type theory (DTT),

DTT ⊢ Γ|φ iff, for every lccc C, C ⊨ Γ|φ.

Since every Π–pretopos is locally cartesian closed we obtain the following:

1.4. Corollary. [Π-Pretopos Soundness and Completeness] For any judgment in context Γ|φ of dependent type theory,

DTT ⊢ Γ|φ iff, for every Π-pretopos R, R ⊨ Γ|φ.

Proof. Soundness is trivial since every Π-pretopos is locally cartesian closed. For completeness notice that if C is locally cartesian closed, then the Yoneda embedding y : C [figure] Ĉpreserves all of the locally cartesian closed structure and Ĉis a Π-pretopos. Suppose that, for all Π-pretopoi R, R ⊨ Γ|φ. Then, in particular, Ĉ ⊨ Γ|φ for every LCCC C. But since y is conservative (i.e., reflects isomorphisms) and preserves lcc structure it follows that C ⊨ Γ|φ. By the foregoing theorem we therefore have ⊢ Γ|φ.

2. Constructive Set Theories

All of the set theories under consideration are first-order intuitionistic theories in the language L := {S, ∈} where S (‘sethood’) and ∈ (‘membership’) are, respectively, unary and binary predicates. We include S in the language because we intend to allow urelements or non-sets. The majority of the results of this section are to be found, either explicitly or implicitly, in [Aczel and Rathjen, 2001] or [Awodey et al, 2004].

Where φ is a formula, FV(φ) denotes the set of free variables of φ. We will freely employ the class notation {x|φ} as in common set theoretical practice. Frequently it will be efficacious to employ bounded quantification which is defined as usual:

∀x ∈ y.φ(x) := ∀x.x ∈ y ⇒ φ(x) and ∃x ∈ y.φ(x) := ∃x.x ∈ y ∧ φ(x).

A formula φ is called Δ_{0} if all of its quantifiers are bounded.

Another notational convenience is the introduction of the ‘set-many’ quantifier S defined as:

Sx.φ := ∃y.(S(y) ∧ ∀x.(x ∈ y ⇔ φ)),

4  STEVE AWODEY AND MICHAEL A. WARREN

where y ∉ FV(φ). We also write:

x ⊆ y := S(x) ∧ S(y) ∧ ∀z ∈ x.z ∈ y.

We write func(f, a, b) to indicate that f is a functional relation on a × b (which will exist in any of the set theories we consider):

func(f, a, b) := f ⊆ a × b ∧ ∀x ∈ a.∃!y ∈ b.(x, y) ∈ f

Finally, for any formula φ, we define:

coll(x ∈ a, y ∈ b, φ) := (∀x ∈ a.∃y ∈ b.φ) ∧ (∀y ∈ b.∃x ∈ a.φ).

For the sake of brevity we omit the obvious universal quantifiers in the following axioms and schemata for set theories: Membership: x ∈ a ⇒ S(a). Universal Sethood: S(x). Extensionality: (a ⊆ b ∧ b ⊆ a) ⇒ a = b. Emptyset: Sz.⊥. Pairing: Sz.z = x ∨ z = y. Binary Intersection: S(a) ∧ S(b) ⇒ Sz.z ∈ a ∧ z ∈ b. Union: S(a) ∧ (∀x ∈ a.S(x)) ⇒ Sz.∃x ∈ a.z ∈ x. Infinity: ∃a.S(a) ∧ (∃x.x ∈ a ∧ (∀x ∈ a)(S(x) ∧ ∃y ∈ a.S(y) ∧ x ∈ y)). ∈-Induction: [∀a.(S(a) ∧ ∀x ∈ a.φ(x) ⇒ φ(a))] ⇒ ∀a.(S(a) ⇒ φ(a)). Replacement: S(a) ∧ ∀x ∈ a.∃!y.φ ⇒ Sy.∃x ∈ a.φ Strong Collection: S(a) ∧ (∀x ∈ a.∃y.φ) ⇒ ∃b.(S(b) ∧ coll(x ∈ a, y ∈ b, φ). Exponentiation: S(a) ∧ S(b) ⇒ Sz.func(z, a, b). Subset Collection: S(a) ∧ S(b) ⇒

∃c.S(c) ∧ [∀v.∀x ∈ a.∃y ∈ b.φ ⇒ ∃d ∈ c.S(d) ∧ coll(x ∈ a, y ∈ d)φ].

Δ_{0}-Separation: S(a) ⇒ Sz.z ∈ a ∧ φ, if φ is a Δ_{0} formula.

Axioms  BCST CST CZF
Membership  •  •  ∘
Extensionality, Pairing, Union  •  •  •
Emptyset  •  •  ∘
Binary Intersection  •  •  ∘
Replacement  •  •  ∘
Δ_{0}-Separation  ∘  ∘  •
Exponentiation  •  ∘
Infinity  •
∈-Induction  •
Strong Collection  •
Subset Collection  •
Universal Sethood  •

Table 1: Several Constructive Set Theories

The particular set theories with which we will be primarily concerned are given in Table 1. In Table 1 we employ a solid bullet • to indicate that the axiom in question is one of the axioms of the theory and a hollow bullet ∘ to indicate a consequence of the axioms. There are several points worth mentioning in connection with Table 1. First, CZF is conventionally formulated in the language {∈} with all of the axioms suitably reformulated. In the present setting this amounts to the addition of Universal Sethood. Secondly, the form of Δ_{0}-Separation which holds in BCST and CST is subject to the stipulation that φ is also well-typed in a sense which will be made precise shortly. Finally, the reader should note that although the theories we consider do not include an axiom of infinity the results of this paper are easily extended to theories augmented with (an appropriate version of) Infinity (to be discussed below).

We begin by showing that a particularly useful axiom schema holds in BCST; namely, Indexed Union:

S(a) ∧ (∀x ∈ a.Sy.φ) ⇒ Sy.∃x ∈ a.φ.

2.1. Lemma. BCST ⊢ Indexed Union.

Proof. Suppose S(a) and ∀x ∈ a.Sy.φ(x, y), then for any x ∈ a there is a unique b such that S(b) and (∀y)(y ∈ b ⇔ φ(x, y)). By Replacement there exists a c such that S(c) and:

c = {z|∃x ∈ a.S(z) ∧ (∀y)(y ∈ z ⇔ φ(x, y))}.

Clearly S(y′) for any y′ ∈ c. By Union S(⋃ c). Intuitively, we want to show that the class w := {z|∃x ∈ a.φ(x, z)} is a set. The claim then is that w = ⋃ c.

To see that this is so suppose that y ∈ ⋃ c. Then there exists a d ∈ c such that y ∈ d. By the definition of c there exists an e ∈ a with (∀z)(z ∈ d ⇔ φ(e, z)). So, since y ∈ d it follows that φ(e, y) and y ∈ w.

Next, suppose that y ∈ w. Then there exists an e ∈ a such that φ(e, y). By the original assumption there exists a set d such that:

d := {z|φ(e, z)}.

Also d ∈ c and since φ(e, y) it follows that y ∈ d and y ∈ ⋃ c. Thus, Sy.∃x ∈ a.φ, as required.

We now show that, although BCST lacks a separation axiom, it is possible to recover some degree of separation. To this end we define:

φ[a, x]-Sep := S(a) ⇒ Sx.(x ∈ a ∧ φ).

Here the free variables a and x need not occur in φ. Additionally we say that a formula φ is simple when the following, written !φ, is provable:

Sz.(z = ∅ ∧ φ)

and z ∉ FV(φ). The intuition behind simplicity is that certain formulas are sufficiently lacking in logical complexity that their truth values are indeed sets. In particular, we will write t_{φ} for {z|z = ∅ ∧ φ} which we call the truth value of φ (and, if necessary, we will exhibit the free variable of φ: t_{φ(x)}). Separation holds for such simple formulae:

2.2. Lemma. [Simple Separation] BCST ⊢ (∀x ∈ a.!φ(x)) ⇒ φ[a, x]-Sep.

Proof. We will show that, given the assumptions, {z|z = x ∧ φ(x)} is a set for each x ∈ a. The conclusion then is an easy consequence of Union-Rep. By assumption S(a) and for every x ∈ a the truth value:

t_{φ(x)} := {z|z = ∅ ∧ φ(x)}

of φ(x) is a set. Suppose y ∈ t_{φ(x)}, then y = ∅ ∧ φ(x). But then ∃!z.z = x ∧ y = ∅ ∧ φ(x). By Replacement:

q := {z|∃y ∈ t_{φ(x)}.z = x ∧ y = ∅ ∧ φ(x)}

is a set. But ∃y ∈ t_{φ(x)}.z = x ∧ y = ∅ ∧ φ(x) is equivalent to z = x ∧ φ(x) so that {z|z = x ∧ φ(x)} is a set, as required.

2.3. Lemma. BCST proves the Equality Axiom (cf. [Simpson, 2004]):

∀x, y.Sz.z = x ∧ z = y.

Proof. Let x and y be given. Then {x} and {y} are sets and, by Binary Intersection, their intersection {x} ∩ {y} is also a set which has the required property.

PREDICATIVE ALGEBRAIC SET THEORY  7

Henceforth, given x and y, we write δ_{xy} for the set {z|z = x ∧ z = y}. 2.4. Lemma. In BCST:

1. !(a = b).

2. If S(a) and ∀x ∈ a.!φ(x), then !(∃x ∈ a.φ(x)) and !(∀x ∈ a.φ(x)).

3. !(x ∈ a), when S(a).

4. If !φ and !ψ, then !(φ ∧ ψ), !(φ ∨ ψ), !(φ ⇒ ψ), and !(¬φ).

5. If φ ∨ ¬φ, then !φ. Proof. See [Awodey et al, 2004] or [Warren, 2004]. 2.5. Corollary. Given the other axioms of BCST the following are equivalent:

1. Binary Intersection,

2. Equality, and

3. Intersection. Proof. See [Awodey et al, 2004] or [Warren, 2004]. 2.6. Definition. Let a Δ_{0} formula φ and a variable x occurring in φ be fixed. We say that x is an orphan if x ∈ FV(φ). If x ∉ FV(φ), then we define the parent of x in φ to be the variable y such that x occurs as a bound variable of one of the following forms in φ: ∀x ∈ y or ∃x ∈ y (note that every x which is not an orphan has a unique parent in φ). The family tree of x in φ, denoted by Φ(φ, x), is the singleton {x} if x is an orphan and otherwise it is the tuple ⟨x, y_{1}, y_{2}, …, y_{n}⟩ such that the following conditions are satisfied:

(i) y_{1} is the parent of x in φ, (ii) each y_{m+1} is the parent of y_{m} for 1 ≤ m ≤ n − 1, and (iii) y_{n} is an orphan. The reader may easily verify that, for each variable x occurring in φ, Φ(φ, x) is unique. 2.7. Definition. Given a Δ_{0} formula φ and a variable x occurring in φ we adopt the following abbreviation:

S(Φ(φ, 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),

where Φ(φ, x) = ⟨x, y_{1}, …, y_{n−1}, y_{n}⟩.

2.8. Definition. If φ is a Δ_{0} formula of BCST such that there are no occurrences of the S predicate in φ and x_{1}, …, x_{n} are all of those variables of φ either bound or free which occur on the right hand side of the ∈ predicate in φ, then we define a formula τ(φ, m) for each 1 ≤ m ≤ n inductively by:

τ(φ, 0) := ⊤.
τ(φ, m + 1) := τ(φ, m) ∧ S(Φ(φ, x_{m+1})).

Then τ(φ) := τ(φ, n).

2.9. Corollary. [Δ_{0}-Separation] If φ is a Δ_{0} formula in which there are no occurrences of S and x_{1}, …, x_{n} are all of those free variables of φ that occur on the right hand side of occurrences of ∈, then:

BCST ⊢ τ(φ) ∧ S(y) ⇒ Sz ∈ y.φ.

2.10. Remark. If the Simple Sethood axiom, which states that the sethood predicate S is simple, is satisfied then full Δ_{0}-separation holds.

We will now show that the category of sets of BCST form a Heyting pretopos and that the sets of CST form a Π-pretopos (what we mean by ‘the category of sets’ will be made precise shortly). First, we consider quotients of equivalence relations.

2.11. Lemma. If S(a) and r ⊆ a × a is an equivalence relation, then for each x ∈ a the equivalence class:

[x]_{r} := {z|z ∈ a ∧ (x, z) ∈ r}

is a set.

Proof. Let x ∈ a be given to show that Sz.z ∈ a ∧ (x, z) ∈ r. In order to apply Simple Separation let an arbitrary y ∈ a be given. It is an obvious consequence of part (2) of Lemma 2.4 that ∀z ∈ r.!(z = (x, y)). By part (1) of the lemma !(∃z ∈ r.z = (x, y)). Since we shown that, for all y ∈ a, !(∃z ∈ r.z = (x, y)) it follows from Simple Separation that Sy.(y ∈ a ∧ (∃z ∈ r.z = (x, y)). I.e., [x]_{r} is a set, as required.

2.12. Lemma. If S(a) and r ⊆ a × a is an equivalence relation, then the quotient

a/r := {[x]_{r}|x ∈ a}

of the set a modulo r is a set.

Proof. This is an easy application of Replacement.

Let “Sets” be the category consisting of sets and functions between them in BCST. More precisely, objects are those x of BCST such that S(x) and arrows f : x [figure] y are those f of BCST such that func(f, x, y). By the foregoing lemmas and some obvious facts that we omit, we have the following:

2.13. Theorem. BCST proves that “Sets” is a Heyting pretopos.

Now we regard “Sets” as the category of sets in CST:

2.14. Lemma. For any object I of “ Sets”, the category “Sets”/I is equivalent to “Sets”^{I} where I is regarded as a discrete category.

Proof. The usual proof goes through in BCST: Define F : “Sets”/I [figure] “Sets”^{I} by:

X [figure: f] I [figure] (X_{i})_{i∈I}, and
h : f [figure] g [figure] (h_{i})_{i∈I},

where X_{i} is the fiber f^{−1}(i) of f over i and:

[figure: X; I; f; X; Y; h; Y; I; g]

commutes in “Sets”. Notice that each X_{i} is a set by Simple Separation.

Let G : “Sets”^{I} [figure] “Sets”/I by:

(X_{i})_{i∈I} [figure] f : X [figure] I,

where X := ∐ X_{i} and, for any x ∈ X, f(x) is the i ∈ I such that x ∈ X_{i}. Here ∐ X_{i} := {(x, i)|x ∈ X_{i}} is a set by Simple Separation.

It is easily verified that F and G constitute an equivalence of categories just as in classical set theory.

Given f : X [figure] Y the pullback functor Δ_{f} : “Sets”/Y [figure] “Sets”/X serves to reindex a family of sets (C_{y})_{y∈Y} as (C_{f(x)})_{x∈X}. Note also that given a set I and a family of sets X_{i} for each i ∈ I, the class {X_{i}|i ∈ I} is a set by Replacement.

2.15. Lemma. For any map f : X [figure] Y in “Sets”, the pullback functor Δ_{f} : “Sets”/Y [figure] “Sets”/X has both a left adjoint Σ_{f} and a right adjoint Π_{f}.

Proof. We may employ the usual definitions of the adjoints:

“Sets”^{X}  [figure: Σ_{f}] “Sets”^{Y}
[figure: (C_{x})_{x∈X}; (S_{y})_{y∈Y} ,]

where S_{y} := ∐_{f(x)=y} C_{x}, and Π_{f}:

[figure: (C_{x})_{x∈X}; (P_{y})_{y∈Y} ,]

where P_{y} := ∏_{f(x)=y} C_{x}. Here the arbitrary product:

∏_{i∈I} X_{i} := {f : I [figure]⋃_{i∈I} X_{i}|∀i ∈ I.f(i) ∈ X_{i}}

is a set. In particular, ⋃ X_{i} is a set by Union and (⋃ X_{i})^{I} is a set by Exponentiation. The result follows directly from Lemma 2.4 and Simple Separation.

By the foregoing lemmas we have proved:

2.16. Theorem. CST proves that “Sets” is a Π-pretopos.

We now consider the theories obtained by augmenting BCST and CST with an axiom of infinity. In what follows we will consider an extension of the language L of set theory obtained by adding three new constants o, s, N (cf. [Simpson, 2004]). We write L^{+} for the language so obtained. Let ψ denote the conjunction of the following three formulae:

∀x ∈ N.o ≠ s(x),

∀x, y ∈ N.s(x) = s(y) ⇒ x = y, and

∀a.[a ⊆ N ∧ o ∈ a ∧ ∀x ∈ a.(s(x) ∈ a)] ⇒ N = a,

then we may state the particular axiom of infinity (Infinity∗) with which we will be concerned:

Infinity∗: S(N) ∧ o ∈ N ∧ func(s, N, N) ∧ ψ.

Henceforth we denote the theory obtained by adding Infinity∗ to BCST by BCST^{+} and similarly for CST. The immediate point to note about the particular axiom of infinity adopted is that it places no unnecessary constraints on the actual elements of N. In particular, we do not know that the elements of N are built up using Pairing and the emptyset; indeed, the elements of N need not even be sets. The benefits of adopting such an axiomatization are both practical and ideological; for such an axiomatization allows us greater ease in the later interpretation of the set theory and permits an ‘implementationinvariance’ not otherwise possible.

For any formula φ, we write φ[x]-Ind for the formula asserting that the axiom of induction holds for φ; namely:

[φ(o) ∧ ∀x ∈ N.(φ(x) ⇒ φ(s(x)))] ⇒ ∀x ∈ N.φ(x).

Then we have the following useful fact:

2.17. Proposition. [Simple Induction] BCST^{+} ⊢ ∀x ∈ N.!φ ⇒ φ[x]-Ind.

Proof. See [Awodey et al, 2004] or [Warren, 2004].

3. Predicative Categories of Classes

In this section we introduce the axiomatic theory of categories of classes (as well as several variants of this notion) and derive soundness and completeness results for BCST and CST. Our approach is related to those developed in [Joyal and Moerdijk, 1995], [Simpson, 1999], [Butz, 2003], [Awodey et al, 2004], and [Rummelhoff, 2004].

3.1. Axioms for Categories with Basic Class Structure. A system of small maps in a positive Heyting category C is a collection S of maps of C satisfying the following axioms:

(S1) S is closed under composition and all identity arrows are in S.

(S2) If the following is a pullback diagram:

[figure: D′; D; g; C′; D′; f′; C′; C; g′; C; D; f]

and f is in S, then f′ is in S.

(S3) All diagonals Δ : C [figure] C × C are contained in S.

(S4) If e is a cover, g is in S and the diagram:

[figure: C; A; g; C; D; e; D; A; f]

commutes, then f is in S.

(S5) If f : C [figure] A and g : D [figure] A are in S, then so is the copair [f, g] : C + D [figure] A.

A map f is small if it is a member of S and an object C is small if the canonical map !_{C} : C [figure] 1 is small. Similarly, a relation R [figure] C × D is a small relation if the composite:

R [figure] C × D [figure] D

with the projection is a small map. Finally, a subobject A [figure] C is a small subobject if A [figure] C × 1 is a small relation; i.e., provided that A is a small object.

3.2. Definition. A category with basic (predicative) class structure is a positive Heyting category C with a system of small maps satisfying:

(P1) For each object C of C there exists a (predicative) power object P_{s} (C) and a small membership relation ϵ_{C} [figure] C × P_{s} (C) such that, for any D and small relation R [figure] C × D, there exists a unique map ρ : D [figure] P_{s} C such that the square:

[figure: C × D; C × P_{s} C; 1_{C}×ρ; R; C × D; R; ϵ_{C}; ϵ_{C}; C × P_{s} C]

is a pullback.

As in topos theory we call the unique map ρ in (P1) the classifying map of R and R the relation classified by ρ.

By the definition of small subobjects and small relations there are covariant functors SSub_{C}(−) and SRel_{B}(−) induced by restricting, for any objects A and B, the covariant ‘direct image’ functors Sub_{C}(B) and Sub_{C}(B × A) to the subposets of small subobjects of B and small relations on B ×A, respectively (this fact requires images of small subobjects to be small which follows by (S4)). The content of the small powerobject axiom (P1) is then that these functors are representable in the sense that:

Hom(A, P_{s} B) ≅ SRel_{B}(A), and
Hom(1, P_{s} B) ≅ SSub_{C}(B).

These facts are proved below in proposition 3.8.

3.3. The Internal Language of Categories with Basic Class Structure. We will now develop some of the properties of the internal language of categories with basic class structure. This approach is influenced by the work of Rummelhoff [Rummelhoff, 2004] and will provide a useful stepping stone for deriving further results. In particular, our aim in developing the internal logic explicitly is twofold:

1. By deriving typed versions of the set theoretic axioms with which we are concerned we are able to provide more elegant soundness proofs; for the validity of the untyped axioms ultimately rests on the validity of their typed analogues.

2. Furthermore, we will make some use of the internal language to show that the subcategories of small things have certain category theoretic properties. E.g., if C is a category with basic class structure, then the subcategory S_{C} of small objects is a Heyting pretopos.

More generally, the development of the theory via the internal language allows us to emphasize the contribution of the categorical structure already present in categories with basic class structure and to compare it with the additional structure provided by the move to categories of classes (cf. subsection 3.32 below).

Henceforth we will assume that the ambient category C is a category with basic class structure. We will denote by π_{A} the composite:

π_{A} : ϵ_{A} [figure] A × P_{s} [figure] P_{s} A.

Throughout we employ infix notation for certain distinguished relations and maps as in the use of x ϵ_{C} y for the more cumbersome ϵ_{C} (x, y). We abbreviate ∀x_{1} : X_{1}.∀x_{2} : X_{2}.∀ ….∀x_{n}.X_{n}.φ by ∀x_{1} : X_{1}, x_{2} : X_{2}, …, x_{n} : X_{n}.φ and similarly for existential quantifiers. Finally, we write ∀x ϵ_{C} y in place of ∀x : C.x ϵ_{C} y.

3.4. Proposition.

1. A relation R [figure] C × D is small iff, for some

ρ : D [figure] P_{s} C:

C ⊨ ∀x : C, y : D.R(x, y) ⇔ x ϵ_{C} ρ(y).

2. A map f : C [figure] D is small iff, for some f^{−1} : D [figure] P_{s} C:

C ⊨ ∀x : C, y : D.f(x) = y ⇔ x ϵ_{C} f^{−1}(y).

Proof. Immediate from the definitions of small maps and relations. In particular, the map f^{−1}, which we call the fiber map, classifies the graph Γ(f) [figure] C × D of f.

The following proposition will be one of the most useful tools at our disposal in the study of categories with basic class structure. Indeed, this proposition serves to establish the importance of axiom (S3) (which will become all the more obvious with the introduction of the category of ideals below.

3.5. Proposition. The following are equivalent given (S1), (S2) and (P1) (cf. [Awodey et al, 2004] and [Rummelhoff, 2004]):

1. (S3).

2. Regular monomorphisms are small.

3. If g ∘ f is small then f is small.

4. ∈_{C}: ϵ_{C} [figure] C × P_{s} C is a small map.

5. [[x : C, u : P_{s} C, v : P_{s} C|x ϵ_{C} u ∧ x ϵ_{C} v]] is a small relation

6. Sections are small.

Proof. For (1)⇒(2) notice that Δ is a regular mono and suppose that m : A [figure] B is the equalizer of h, k : B [figure] C. Then:

[figure: B; C × C; ⟨h,k⟩; A; B; m; A; C; h∘m=k∘m; C; C × C; Δ]

is a pullback and m is small by (S2).

To show that (2)⇒(3) suppose regular monos are small and g ∘ f is small where:

A [figure: f] B [figure: g] C,

and consider the pullback:

[figure: A; C.; g∘f; P; A; p_{1}; P; B; p_{2}; B; C.; g]

There is a canonical map ζ : A [figure] P such that p_{1} ∘ ζ = 1_{A}. By (S1) f is a small map.

(3)⇒(1) is trivial. Also (3)⇒(4) is trivial. (4)⇒(1) is by (S2). Both (3)⇒(6) and (6)⇒(1) are trivial.

For (4)⇒(5) notice that if R [figure] C × D is a small relation and the map S [figure] C × D is small, then R ∧ S is a small relation. (5)⇒(1) is by the fact that:

C ⊨ ∀x : C, y : C.x = y ⇔ ∀z : C.z ϵ_{C} {x}_{C} ∧ z ϵ_{C} {y}_{C}.

3.6. Corollary. All of the canonical maps !_{A} : 0 [figure] A are small and if f : A [figure] B and g : C [figure] D are small, then f + g : A + C [figure] B + D is also small.

The reader should be alerted at this point that use of proposition 3.5 and its corollary will often be made without explicit mention.

3.7. Proposition. [Typed Axioms] The following are true in any category C with basic class structure:

Extensionality: For any object C:

C ⊨ ∀a, b : P_{s} C.(∀x : C.x ϵ_{C} a ⇔ x ϵ_{C} b) ⇒ a = b.

Emptyset: For each object C there exists a map ∅_{C} : 1 [figure] P_{s} C such that:

C ⊨ ∀x : C.x ϵ_{C} ∅_{C} ⇔ ⊥.

Singleton: For each object C the singleton map {−}_{C}, which is the classifying map for the diagonal Δ : C [figure] C × C, is a small monomorphism.

Binary Union: For each C there exists a map ∪_{C} : P_{s} C × P_{s} C [figure] P_{s} C such that:

C ⊨ ∀x : C, a, b : P_{s} C.x ϵ_{C} (a ∪_{C} b) ⇔ x ϵ_{C} a ∨ x ϵ_{C} b.

Product: For all C and D there exists a map ×_{C,D} : P_{s} C × P_{s} D [figure] P_{s} (C × D) such that:

C ⊨ ∀x : C, y : D, a : P_{s} C, b : P_{s} D.(x, y) ϵ_{C×D} (a ×_{C,D} b) ⇔ x ϵ_{C} a ∧ y ϵ_{D} b.

Pairing: For any C there exists a map {−, −}_{C} : C × C [figure] P_{s} C such that:

C ⊨ ∀x, y, z : C.x ϵ_{C} {y, z}_{C} ⇔ x = y ∨ x = z.

Proof. For Extensionality, let the subobject r be given by the following:

[[a, b : P_{s} C|(∀x : C)(x ϵ_{C} a ⇔ x ϵ_{C} b)]] [figure: r] P_{s} C × P_{s} C.

By (P1) there exist subobjects S, S′ of C × R classified by π_{1} ∘ r and π_{2} ∘ r, respectively. But by assumption S = S′. Notice that r factors through the diagonal Δ iff π_{1} ∘r = π_{2} ∘r (recall that Δ is the equalizer of π_{2} and π_{2}). Thus, by (P1), R factors through Δ, as required.

For Emptyset it suffices to notice that [[x : C|⊥]] is small.

For Singleton note that by Proposition 3.4 we have that:

[[x, y : C|x ϵ_{C} {y}]] = Δ,

so that if C ⊨ {x}_{C} = {y}_{C}, then C ⊨ x = y. To see that {−}_{C} is small notice that where:

[figure: C × C; C × P_{s} C; 1_{C}×{−}_{C}; C; C × C; Δ; C; ϵ_{C}; p; ϵ_{C}; C × P_{s} C; ∈_{C}]

we have {−}_{C} = π_{C} ∘ p. But p is small since it has a retraction.

Binary Union follows from the fact that, by (S4) and (S5), the join of two small subobjects is a small subobject. Product is by (S2). Finally, for Pairing, the map {−, −}_{C} : C × C [figure] P_{s} C is the composite ∪_{C} ∘ ({−}_{C} × {−}_{C}).

The foregoing is a good start, but before we are able to verify that more sophisticated principles (e.g., Replacement) we must first develop several additional properties of the categories in question.

3.8. Proposition. P_{s} (−) is the object part of a covariant endofunctor P_{s} on C.

Proof. As in [Joyal and Moerdijk, 1995] or [Awodey et al, 2004].

16  STEVE AWODEY AND MICHAEL A. WARREN

Henceforth we write f_{!} : P_{s} C [figure] P_{s} D instead of P_{s} (f), where f : C [figure] D. 3.9. Proposition. Where f : C [figure] D:

C ⊨ ∀x : D, a : P_{s} C.x ϵ_{D} f_{!}(a) ⇔ ∃y ϵ_{C} a.f(y) = x.

Proof. Easy. 3.10. Corollary. If m : C [figure] D is monic, then so is m_{!} : P_{s} C [figure] P_{s} D. I.e.,

C ⊨ ∀x, x′ : P_{s} C.m_{!}(x) = m_{!}(x′) ⇒ x = x′.

Proof. By Typed Extensionality and the internal language. 3.11. Corollary. If m : C [figure] D is monic, then:

[figure: C × P_{s} C; D × P_{s} D; m×m_{!}; ϵ_{C}; C × P_{s} C; ϵ_{C}; ϵ_{D}; ϵ_{D}; D × P_{s} D]

is a pullback. Proof. Easy. 3.12. Proposition. Every small map f : C [figure] D gives rise to an (internal) inverse image map f^{∗} : P_{s} D [figure] P_{s} C. Proof. As in [Joyal and Moerdijk, 1995] or [Awodey et al, 2004]. 3.13. Proposition. If f : C [figure] D is a small map, then:

C ⊨ ∀x : C, a : P_{s} D.x ϵ_{C} f^{∗}(a) ⇔ f(x) ϵ_{D} a,

where f^{∗} is as above. Proof. Easy.

In the following we write ⊆_{C} for the subobject of P_{s} C × P_{s} C given by:

⊆_{C} := [[x : P_{s} C, y : P_{s} C|∀z ϵ_{C} x.z ϵ_{C} y]].

From this description of ⊆_{C} it easily follows that ⊆_{C} [figure] P_{s} C × P_{s} C is the equalizer of π_{1}, ∩_{C} : P_{s} C × P_{s} C [figure] P_{s} C and that:

C ⊨ ∀x, y : P_{s} C.x ⊆_{C} y ⇔ x ∩_{C} y = x.

3.14. Lemma. If f : C [figure] D is a small map, then f_{!} ⊣ f^{∗} internally. That is:

C ⊨ ∀x : P_{s} C, y : P_{s} D.f_{!}(x) ⊆_{D} y ⇔ x ⊆_{C} f^{∗}(y).

Proof. Easy using the internal language.

3.15. Proposition. [Internal Beck-Chevalley Condition] If f : C [figure] D is a small map and the following diagram is a pullback:

[figure: D′; D; g; C′; D′; f′; C′; C; g′; C; D; f]

then f^{∗} ∘ g_{!} = g′_{!} ∘ (f′)^{∗}.

Proof. By the external Beck-Chevalley condition.

3.16. Slicing, Exponentiation and the Subcategory of Small Objects. In this subsection we first show that the structure of categories with basic class structure is preserved under slicing. Next, we show that small objects are exponentiable and introduce the (categorical) exponentiation axiom. Finally, we show that the category S_{C} of small objects in a category C with basic class structure is a Heyting pretopos and, moreover, if C also satisfies the categorical exponentiation axiom, then S_{C} is a Π-pretopos.

3.17. Theorem. If C is a category with basic class structure and D is an object of C, then C/D is also a category with basic class structure.

Proof. The Heyting category structure of C is easily seen to be preserved under slicing. Also, the collection S_{D} of all maps in C/D that are small in C is a system of small maps in C/D.

Where f : C [figure] D is an object in C/D we define the powerobject P_{s} (f : C [figure] D) as the composite p_{f} : V_{f} [figure] P_{s} C × D [figure] D where V_{f} is defined as follows:

V_{f} := [[x : P_{s} C, y : D|f_{!}(x) ⊆_{D} {y}_{D}]].

Notice that by previous results V_{f} = [[x, y|∀z ϵ_{C} x.f(z) = y]]. Similarly, we define the membership relation ϵ_{f} as the composite M_{f} [figure] D × C × P_{s} C [figure] D where:

M_{f} := [[x : D, y : C, z : P_{s} C|y ϵ_{C} z ∧ ∀x′ ϵ_{C} z.f(x′) = x]].

For further details see [Awodey et al, 2004] or [Warren, 2004].

3.18. Lemma. Given f : B [figure] A in C the pullback functor Δ_{f} : C/A [figure] C/B preserves all basic class structure.

Proof. See [Warren, 2004].

We will now show that exponentials D^{C} exist when C is a small object. We define the exponential in question as a subobject of P_{s} (C × D) as follows:

D^{C} := [[R : P_{s} (C × D)|∀x : C.∃!y : D.(x, y) ϵ_{C×D} R]].

3.19. Lemma. If C is small, then the following special case of the adjunction − × C ⊣ −^{C} holds:

Hom(C, D) ≅ Hom(1, D^{C})  (1)

That is to say, there exists a natural isomorphism Hom(C, D) ≅ Hom(1, D^{C}).

Proof. By the internal language (cf. [Warren, 2004]).

Now, using the fact that C/E has basic class structure and the pullback functor Δ_{!_{E}} : C [figure] C/E preserves this structure we arrive at the more general lemma:

3.20. Lemma. Where C is a small object we have the following natural isomorphisms:

Hom(E × C, D) ≅ Hom(E, D^{C})  (2)

3.21. Corollary. Small objects are exponentiable.

3.22. Proposition. If f : C [figure] D is a small map, then the pullback functor Δ_{f} : C/D [figure] C/C has a right adjoint Π_{f}.

Proof. Clearly (f : C [figure] D) is a small object in C/D and, hence, exponentiable there. The existence of the adjoint Π_{f} then follows as usual.

3.23. Definition. A category with (predicative) class structure is a category C with basic class structure which also satisfies the following exponentiation axiom:

(E) If f : C [figure] D is a small map, then the functor Π_{f} : C/C [figure] C/D (which exists by the foregoing proposition) preserves small maps.

3.24. Proposition. In a category with class structure if C and D are both small, then so is D^{C}.

Proof. Notice that D^{C} is Π_{C} ∘ Δ_{C}(D). Moreover, since D is small so is Δ_{C}(D). By (E) it follows that D^{C} [figure] 1 is also small.

3.25. Proposition. If C is a category with class structure and D is an object of C, then C/D also has class structure.

Proof. Use the fact that (C/D)/f ≅ C/dom(f).

In the following proposition and theorem we will be concerned with the properties of the full subcategory S_{C} := S/1 of C consisting of small objects and small maps between them.

3.26. Proposition. Let C be a category with basic class structure. If ∂_{0}, ∂_{1} : R [figure] C×C is an equivalence relation in S_{C}, then the coequalizer of ∂_{0} and ∂_{1} exists in S_{C} and ∂_{0}, ∂_{1} is its kernel pair.

Proof. We define the coequalizer C/R by:

C/R := [[z : P_{s} C|∃x : C.∀y : C.y ϵ_{C} z ⇔ R(x, y)]].

Notice that since ∂_{0} and ∂_{1} are small maps so is ⟨∂_{0}, ∂_{1}⟩ : R [figure] C × C. As such, ⟨∂_{0}, ∂_{1}⟩ is also a small relation and there exists a unique α : C [figure] P_{s} C such that:

[figure: C × C; C × P_{s} C; 1×α; R; C × C; R; ϵ_{C}; p; ϵ_{C}; C × P_{s} C]

is a pullback. That is:

C ⊨ ∀x, y : C.R(x, y) ⇔ x ϵ_{C} α(y).  (3)

By (3) and Typed Extensionality it follows that C/R is the image of α:

im(α) = [[z : P_{s} C|∃x : C.α(x) = z]],

and, as such, that α factors through i : C/R [figure] P_{s} C via a cover ᾱ. Moreover, by (P1), ᾱ ∘ ∂_{0} = ᾱ ∘ ∂_{1} since ⟨∂_{0}, ∂_{1}⟩ is an equivalence relation. Notice that since C is small it follows that ᾱ is a small map and, by (S4), that C/R is a small object.

Finally, we will show that ∂_{0}, ∂_{1} is the kernel pair of ᾱ; i.e., that:

[figure: C; C/R; ᾱ; R; C; ∂_{0}; R; C; ∂_{1}; C; C/R; ᾱ]

is a pullback. Let an object Z and maps z_{0}, z_{1} : Z [figure] C be given such that ᾱ ∘ z_{0} = ᾱ ∘ z_{1}. Then we also have that α ∘ z_{0} = α ∘ z_{1}. Define a map η : Z [figure]ϵ_{C} by η := p ∘ r ∘ z_{0}, where r is the ‘reflexivity’ map. Then we have:

∈ ∘η = ⟨∂_{0}, α ∘ ∂_{1}⟩ ∘ r ∘ z_{0}
= ⟨z_{0}, α ∘ z_{0}⟩
= (1_{C} × α) ∘ ⟨∂_{0}, ∂_{1}⟩.

By the universal property of pullbacks there exists a unique map η̄: Z [figure] R with p∘η̄ = η and ⟨∂_{0}, ∂_{1}⟩∘η̄ = ⟨z_{0}, z_{1}⟩. Moreover η̄ is the unique map from Z to R such that ∂_{0} ∘η̄ = z_{0} and ∂_{1} ∘ η̄ = z_{1}. It follows from the fact that covers coequalize their kernel pairs that ᾱ is a coequalizer of ∂_{0} and ∂_{1}. It is easily seen that if Z together with z_{0} and z_{1} are in S_{C}, then so is η̂.

3.27. Theorem. If C has basic class structure, then S_{C} is a Heyting pretopos. Moreover, if C has class structure, then S_{C} is a Π-pretopos.

Proof. By Proposition 3.26 S_{C} has coequalizers of equivalence relations. It suffices to show that S_{C} is a positive Heyting category. But, this structure is easily seen exist since C is a positive Heyting category. For instance, to show that S_{C} has disjoint finite coproducts note that if C and D are small objects then so is C + D together with the maps C [figure] C +D and D [figure] C +D by (S5). Disjointness and stability are consequences of (S3). Similarly, by the description of C × D as the pullback of !_{C} along !_{D}, it follows that C × D is a small object when C and D are. S_{C} is seen to be regular by (S3). Finally, for dual images, let a map f : C [figure] D and a subobject m : S [figure] C be given in S_{C}. Consider the subobject i : ∀_{f}(m) [figure] D. Notice that, in general, if a monomorphism C [figure] D in a category C with basic class structure is small, then it is also regular since it is a pullback of the section ⊤ : 1 [figure] P_{s} 1. Moreover since, by Proposition 3.22, Π_{f} exists and is a right adjoint, it follows that i is a small map.

The further result is a consequence of Proposition 3.24.

3.28. Typed Union and Replacement. We now show that typed versions of Union and Replacement are valid in categories with basic class structure. To this end, we introduce a typed version of the ‘Sz.φ’ notation from above as follows:

Sx : C.φ := ∃y : P_{s} C.∀x : C.(x ϵ_{C} y ⇔ φ),

where y ∉ FV(φ).

3.29. Proposition. A relation R [figure] C × D is small if and only if C ⊨ ∀y : D.Sx : C.R(x, y).

Proof. Suppose R [figure] C × D is a small relation and ρ : D [figure] P_{s} C is the classifying map. Then by Proposition 3.4 we have C ⊨ ∀y : D.∀x : C.R(x, y) ⇔ x ϵ_{C} ρ(y). The conclusion may be seen to follow from this (use ρ to witness the existential).

For the other direction suppose C ⊨ ∀y : D.Sx : C.R(x, y). Then, by Typed Extensionality:

C ⊨ ∀y : D.∃!z : P_{s} C.∀x : C(x ϵ_{C} z ⇔ R(x, y)),

and there is a map ρ : D [figure] P_{s} C with the requisite property.

3.30. Proposition. [Typed Union] For all C:

C ⊨ ∀a : P_{s} (P_{s} C).Sz : C.∃x ϵ_{P_{s} C} a.z ϵ_{C} x.

Proof. Let H be defined as:

H := [[x : C, y : P_{s} C, z : P_{s} (P_{s} C)|y ϵ_{P_{s} C} z ∧ x ϵ_{C} y]],

and note that the projection:

H [figure] C × P_{s} C × P_{s} (P_{s} C) [figure] P_{s} (P_{s} C)

is small. By (S4) it follows that [[x : C, z : P_{s} (P_{s} C)|∃y ϵ_{P_{s} C} z ∧x ϵ_{C} y]] is a small relation. We write ⋃_{C} : P_{s} (P_{s} C) [figure] P_{s} C for the classifying map.

3.31. Proposition. [Typed Replacement] For all C and D:

C ⊨ ∀a : P_{s} C.(∀x ϵ_{C} a.∃!y : D.φ) ⇒ (Sy : D.∃x ϵ_{C} a.φ).

Proof. Let a : 1 [figure] P_{s} C be given with 1 ⊩ ∀x ϵ_{C} a.∃!y : D.φ. Let α [figure] C be the small subobject classified by a. Then the assumption yields a map f : α [figure] C [figure] D such that:

Γ(f) = [[x : α, y : D|φ(x, y)]].

Moreover, the image of f is the subobject:

I := [[y : D|∃x ϵ_{C} a.φ(x, y)]].

Since α is a small subobject it follows by (S4) that I is also a small subobject. We may now pull the general problem back as usual.

3.32. Universes and Categories of Classes. All of the set theories introduced earlier are untyped (or, as we prefer to think of things, mono-typed) theories; yet the internal languages of the categories we have been considering are typed languages. As such, we will introduce a technical device which will allow us to model untyped theories. The use of universal objects for this purpose originated in [Simpson, 1999] and has its roots in Scott’s earlier work on modeling the lambda calculus (cf. [Scott, 1980]).

3.33. Definition. A universal object in a category C is an object U of C such that for any object C there exists a monomorphism m : C [figure] U. Similarly, in a category C with basic class structure, a universe is an object U together with a monomorphism ι : P_{s} (U) [figure] U.

Notice that the monomorphisms m and ι in the definition need not be unique. Also, notice that if U is a universe in a category C then we may obtain a category C′ containing a universal object, also U, by restricting to the full subcategory of C consisting of subobjects of U.

3.34. Definition. A basic (predicative) category of classes a category C with basic class structure satisfying the additional universal object axiom:

(U) There exists a universal object U.

Similarly, a predicative category of classes is a category with class structure satisfying (U).

We will now turn to proving that BCST is sound and complete with respect to models in basic categories of classes and that CST is sound and complete with respect to models in predicative categories of classes.

3.35. Soundness and Completeness. In order to interpret the theories in question in basic categories of classes (respectively, predicative categories of classes) we must choose a monomorphism ι : P_{s} U [figure] U (this is because (U) is consistent with the existence of multiple monos P_{s} U [figure] U). An interpretation of BCST in a basic category of classes C is a conventional interpretation [[−]] of the first-order structure (∈, S) determined by the following conditions:

• [[S(x)]] is defined to be:

P_{s} U [figure: ι] U.

• [[x ∈ y]] is interpreted as the subobject:

ϵ_{U} [figure: ∈] U × P_{s} U [figure: 1×ι] U × U.

3.36. Remark. We write (C, U) ⊨ φ to indicate that φ is satisfied by the interpretation. As above C ⊨ φ indicates that φ is true in the internal language and Z ⊩ φ means that Z forces φ. We will now derive several useful results that will allow us to transfer results about the typed internal language to the untyped set theories in question.

3.37. Lemma. If m : C [figure] D is a small map and r : R [figure] D × E is a small relation with classifying map ρ : E [figure] P_{s} D such that E ⊩ ∀z ϵ_{D} ρ.φ(z), where we write [[x : D|φ]] for C as a subobject of D, then there exists a restriction r′ : R′ [figure] C × E of R to C which is a small relation with classifying map ρ′ : E [figure] P_{s} C such that ρ = m_{!} ∘ ρ′.

Proof. Let r′ : R′ [figure] C × E be the pullback of r : R [figure] D × E along m × 1_{E}, then, since m × 1_{E} is small r′ : R′ [figure] C × E is a small relation and there exists a classifying map ρ′ : E [figure] P_{s} C.

We use (P1) to show that ρ = m_{!} ∘ ρ′. In particular, let p : P [figure] D × E be the small relation which results by pulling ϵ_{D} back along 1 × (m_{!} ∘ ρ′), then it is a straightforward application of the internal language to show that the following holds:

C ⊨ ∀x : D, y : E.x ϵ_{D} ρ(y) ⇔ x ϵ_{D} m_{!} ∘ ρ′(y).

By (P1) it follows that ρ = m_{!} ∘ ρ′.

3.38. Proposition. Suppose i : α [figure] C is a small map, then:

P_{s} α = [[x : P_{s} C|∀z ϵ_{C} x.α(z)]],

where P_{s} α is regarded as a subobject of P_{s} C via i_{!} : P_{s} α [figure] P_{s} C. In particular, when α is a small subobject with classifying map a : 1 [figure] P_{s} C we have:

P_{s} α = [[x : P_{s} C|x ⊆_{C} a]].

Proof. Writing [[x : P_{s} C|ψ]] for P_{s} α as a subobject of P_{s} C we must show that:

C ⊨ ∀x : P_{s} C.ψ(x) ⇔ ∀z ϵ_{C} x.α(z).

The left-to-right direction is a straightforward application of the internal language. The right-to-left direction is by Lemma 3.37.

3.39. Lemma. If a : 1 [figure] U and 1 ⊩ S(a) via some map ā : 1 [figure] P_{s} U, then:

[[x|S(x) ∧ (∀y)(y ∈ x ⇒ y ∈ a)]] = P_{s} α,

where i : α [figure] U is the small subobject classified by ā and P_{s} α is regarded as a subobject of U via ι ∘ i_{!}.

Proof. Note that [[x, z|(∀y)(y ∈ x ⇒ y ∈ z)]] is the composite:

⊆_{U} [figure: j] P_{s} U × P_{s} U [figure: ι×ι] U × U.

Using Proposition 3.38 the proof is by the following diagram:

[figure: P_{s} U; U; ι; P_{s} U; P_{s} U; 1; P_{s} U; P_{s} U; 1; P_{s} U; U; ι; U; U × U.; 1×a; P_{s} U; U; ι; P_{s} U; P_{s} U × P_{s} U; 1×ā; P_{s} U × P_{s} U; U × U.; ι×ι; P_{s} U; P_{s} U; 1; P_{s} α; P_{s} U; i_{!}; P_{s} α; P_{s} α; 1; P_{s} α; P_{s} U; i_{!}; P_{s} U; P_{s} U × P_{s} U; 1×ā; P_{s} α; P_{s} U; i_{!}; P_{s} α; ⊆_{U}; ⊆_{U}; P_{s} U × P_{s} U; j]

3.40. Theorem. [Soundness of BCST] BCST is sound with respect to models in basic categories of classes.

Proof. The Membership axiom is trivial and all of the other axioms follow from the previous results contained in this subsection and the fact that their typed analogues are valid in the internal languages of categories with basic class structure (see 3.7, 3.30 and 3.31).

In order to prove the soundness of CST we will need a way to eliminate the defined terms such as func(f, a, b), {a, b}, et cetera which occur in Exponentiation. We now prove several lemmas which will provide us with the requisite methods (which will also be needed to prove the soundness of BCST^{+}).

3.41. Lemma. [Eliminating Defined Terms] In any basic category of classes C:

1. Given a : 1 [figure] U (such an a will usually occur for us as the interpretation of a constant) we have that [[{a}]] = ι ∘ {−}_{U} ∘ a.

2. If a, b : 1 [figure] U, then [[{a, b}]] = ι ∘ {−, −}_{U} ∘ ⟨a, b⟩.

3. There exists a map pair : U × U [figure] U such that, given a, b as above, pair(⟨a, b⟩) = [[⟨a, b⟩]] (in the latter the ⟨a, b⟩ is the set theoretic, defined, ordered pair).

Proof. See [Warren, 2004].

3.42. Lemma. Let a, b : 1 [figure] U each factoring through ι via maps ā, b̄: 1 [figure] P_{s} U be given, then [[a × b]] = ι ∘ (pair)_{!} ∘ ×_{U,U} ∘ ⟨ā, b̄⟩.

Proof. First, let i : α [figure] U and j : β [figure] U be the small subobjects classified by ā and b̄, respectively. Define \overline{a × b} := (pair)_{!} ∘ ×_{U,U} ∘ ⟨ā, b̄⟩ and k := pair ∘ (i × j). It is straightforward to verify that:

[[x : U|x ϵ_{U} \overline{a × b}]] = [[x : U|x ϵ_{U} k]].

The required result then follows by soundness.

3.43. Corollary. If a, b : 1 [figure] U factor through ι via ā and b̄, respectively, and i : α [figure] U and j : β [figure] U are the subobjects classified by ā and b̄, respectively, then:

[[x|S(x) ∧ (∀y)(y ∈ x ⇒ y ∈ a × b)]] = P_{s} (α × β),

where P_{s} (α × β) is regarded as a subobject of U via the map ι ∘ (pair)_{!} ∘ (i × j)_{!}.

Proof. By lemmas 3.42 and 3.39.

3.44. Corollary. Given the same assumptions as in the foregoing corollary:

β^{α} = [[z|z ⊆ a × b ∧ ∀x ∈ a.∃!y ∈ b.⟨x, y⟩ ∈ z]],

where β^{α} is regarded as a subobject of U via the map ι ∘ (pair)_{!} ∘ (i × j)_{!} ∘ l and l : β^{α} [figure] P_{s} (α × β).

Proof. Using the foregoing corollary as well as the internal language.

3.45. Theorem. [Soundness of CST] CST is sound with respect to models in predicative categories of classes.

Proof. All that remains to be checked is that (C, U) ⊨ Exponentiation where C is a predicative category of classes.

We will first show that for any a, b : 1 [figure] U factoring through ι : P_{s} U [figure] U via maps ā and b̄, respectively, the subobject [[z|func(z, a, b)]] is small. By definition there exist small subobjects α and β of U corresponding to ā and b̄.

Since these subobjects are small so is the exponential β^{α} by Proposition 3.24 and, by the foregoing lemma and Proposition 3.38, it follows that:

β^{α} = [[z|z ⊆ a × b ∧ ∀x ∈ a.∃!y ∈ b.⟨x, y⟩ ∈ z]].  (4)

The general result follows from the fact that, given a, b : Z [figure] U such that Z ⊩ S(a)∧S(b), we may pull the problem back to C/Z along Δ_{!_{Z}}.

In order to prove the completeness of BCST with respect to models (C, U) in basic categories of classes and the completeness of CST with respect to models in predicative categories of classes we employ the familiar syntactic category construction. This approach to completeness theorems is to be found in [Awodey et al, 2004] has its origins for the purposes of algebraic set theory in [Simpson, 1999]. For proofs of the relevant facts the reader is referred therefore to [Awodey et al, 2004] and [Warren, 2004].

3.46. Theorem. [Completeness] For any formula φ of L, if (C, U) ⊨ φ for all models (C, U) with C a category of classes, then BCST ⊢ φ. Similarly, if (C, U) ⊨ φ for all models with C a predicative category of classes, then CST ⊢ φ.

Proof. See [Warren, 2004].

We obtain analogous theorems for the theories BCST^{+} and CST^{+} if we restrict attention only to those basic categories of classes (respectively, categories of classes) C such that there exists a natural number object in the subcategory S_{C} of small objects and maps. Explicitly:

3.47. Theorem. For any formula φ of L^{+}, (C, U) ⊨ φ for all models (C, U) with such that C is a basic category of classes and S_{C} has a natural number object if and only if BCST^{+} ⊢ φ (and similarly for CST^{+}).

4. The Ideal Completion of a Pretopos

In this section we construct models of CST ‘over’ Π-pretopoi R. Intuitively, the construction proceeds by freely adjoining certain ‘nice’ colimits to the base category R. This is achieved explicitly by considering a certain subcategory of the category Sh(R) of sheaves over R. Henceforth we assume that sheaves are taken with respect to the coherent coverage (also called the ‘finite-epi’ in pre-Johnstonian terminology).

4.1. Definitions and Basic Properties. Given a category C, recall that the inductive completion Ind(C) is the subcategory of Ĉ consisting of filtered colimits of representables. We will be concerned only with those Ind-objects which are ideals, in the following sense:

4.2. Definition. A diagram D : I [figure] C is an ideal diagram in C provided that I is a small filtered category such that for every map α : i [figure] j in I the map D(α) is a monic. An ideal I on a category C is an object of Ĉ which is (up to isomorphism) a colimit of an ideal diagram of representables.

Using this definition, the ideal completion Idl(C) of a category C is the full subcategory of Ĉ consisting of ideals. Indeed, if C is a pretopos then since every ideal is a sheaf for the coherent coverage (cf. [Awodey and Forssell, 2004]), Idl(C) is also a subcategory of Sh(C).

In Ĉ the representable functors have many nice properties. One such property is that they satisfy a form of compactness (or presentability) condition analogous to the defining condition for compact elements of a lattice:

4.3. Proposition. [Representable Compactness] In Ĉ, where X is a colimit \underrightarrow{lim}_{i} yD_{i} of representables, any map f : yC [figure] X factors through at least one of the canonical maps l_{i} : yD_{i} [figure] X.

Proof. Let X, yC and f be given as in the statement of the theorem and let P := ∐_{i} yD_{i} be the coproduct of the yD_{i}. Then, by the construction of \underrightarrow{lim}_{i} yD_{i} as a coequalizer of coproducts, there is a canonical map ξ : P [figure] X such that each l_{j} : yD_{j} [figure] X factors as l_{j} = ξ ∘ ι_{j}, where ι_{j} : yD_{j} [figure] P is the coproduct inclusion. It is easily verified that ξ is a cover.

Since representables are projective it follows that there is a map ζ : yC [figure] P such that ξ ∘ ζ = f. Therefore there exists a yD_{j} such that ζ factors through some ι_{j} : yD_{j} [figure] P via some map η. But then:

f = ξ ∘ ζ
= ξ ∘ ι_{j} ∘ η
= l_{j} ∘ η,

as required.

Of course, when X is an ideal any such factorization will occur also in Idl(R) since Idl(R) is a full subcategory of R̂.

4.4. Definition. Where C and D are categories with colimits of ideal diagrams, a functor F : D [figure] C is said to be continuous provided that it preserves colimits of ideal diagrams.

4.5. Proposition. If C is a category with colimits of ideal diagrams and R is any category, then any functor F : R [figure] C which preserves monomorphisms extends to a functor F̄ : Idl(R) [figure] C which is continuous and unique up to natural isomorphism. In this sense Idl(R) is the free completion of R with colimits of ideal diagrams:

[figure: R; C.; F; R; Idl(R); y; Idl(R); C.; F̄]

Proof. Let F̄(\underrightarrow{lim}_{i∈I} yC_{i}) := \underrightarrow{lim}_{i∈I} F (C_{i}). Notice that the assumption that F preserves monomorphisms is necessary so that the colimit \underrightarrow{lim}_{i} F (C_{i}) exists in C.

4.6. Class Structure in Idl(C). In explaining the basic class structure on Idl(C) we make use of the intuition that the representables should be the small objects and that the small maps should be those with small fibers. This intuition is made explicit in the following definition:

4.7. Definition. A map f : X [figure] Y in Sh(C) is small provided that it pulls representables back to representables. I.e., f is small provided that, for every yC [figure] Y the object P in the following pullback diagram is a representable:

[figure: X; Y.; f; P; X; P; yC; yC; Y.]

As such, an object is small if and only if it is a representable since the terminal object of Idl(C) is y1.

4.8. Definition. A sheaf F is separated if and only if its diagonal Δ : F [figure] F × F is a small map. Note though that being a separated sheaf is not the same as being a separated presheaf (all sheaves are trivially separated presheaves).

Using this definition of small maps between sheaves we are able to employ a characterization, which was proposed by André Joyal, of the ideals as precisely the separated sheaves. This is stated explicitly in the following theorem.

4.9. Theorem. [The Joyal Condition] Let C be a pretopos, then, for any sheaf F in Sh(C), the following are equivalent:

1. F is an ideal.

2. F is separated.

3. For all arrows f : yC [figure] F with representable domain, the image of f is representable; i.e., f : yC [figure] yD [figure] F for some yD.

Proof. See [Awodey and Forssell, 2004].

Using the Joyal condition one may easily show that Idl(C) has several nice properties.

4.10. Theorem. If C is a pretopos, then:

1. Idl(C) is a positive Heyting category.

2. All of the positive Heyting structure of Idl(C) may be computed in Sh(C).

3. The (restricted) Yoneda embedding y : C [figure] Idl(C) preserves the pretopos structure, all limits existing in C and, moreover, if C is Heyting, then it is a Heyting functor.

Proof. See [Awodey and Forssell, 2004].

Next we show that the small map axioms from 3.1 are satisfied in Idl(C):

4.11. Proposition. Let C be a pretopos, then Idl(C) satisfies axioms (S1)-(S5).

Proof. (S1) and (S2) are easy. (S3) is by the Joyal Condition.

For (S4) suppose we have:

[figure: X; Z; f∘e; X; Y; e; Y; Z; f]

with e a cover and f ∘ e small. Let i : yC [figure] Z be given and consider the diagram:

[figure: X; Y; e; yC′; X; yC′; P; e′; P; Y; Y; Z; f; P; Y; P; yC; f′; yC; Z]

where both squares are pullbacks (as is the outer rectangle). Then it follows that P is representable.

For (S5) notice that the pullback of yC [figure] Z along [f, g] : X +Y [figure] Z is the coproduct f^{∗}(yC)+g^{∗}(yC) which is representable since both f^{∗}(yC) and g^{∗}(yC) are representable.

We will strengthen this result by showing that, where R is a Heyting pretopos, the category Idl(R) is a category with basic class structure. In order to motivate the definition of the (predicative) powerobjects P_{s} (X) in Idl(R) suppose that the indexing category is a topos E and consider a provisional definition of the powerobject of an object yC in Ê as follows:

P_{s} (yC) := y(P(C)),

where P(C) is the usual (topos) powerobject of C in E. Then we have P_{s} (yC) ≅ y(Ω^{C}) and at any object E in E:

P_{s} (yC)(E) ≅ y(Ω^{C})(E)
= Hom_{E}(E, Ω^{C})
≅ Hom_{E}(E × C, Ω)
≅ Sub_{E}(E × C).

Dropping both the assumption that the indexing category is a topos and that we are working in presheaves, we therefore adopt the following provisional definition of the small powerobject of yC in Idl(R):

P_{s} (yC) := Sub_{R}(− × C).

We then extend P_{s} (−) continuously to ideals X = \underrightarrow{lim}_{i} yC_{i} by:

P_{s} (X) := \underrightarrow{lim}_{i} P_{s} (yC_{i}).

We will show that this definition of P_{s} (X) is justified by first showing that there is a functor Sub_{R}^{r} : R [figure] Idl(R) which takes C to Sub_{R}(− × C) and which preserves monomorphisms. Then it will be possible to apply Proposition 4.5 to arrive at an extension P_{s} : Idl(R) [figure] Idl(R) which will be seen to be a powerobject functor in the sense of satisfying (P1).

Similarly, we will define the membership relation ϵ_{X} [figure] X × P_{s} X as the restriction of the sheaf (hence also of the presheaf) membership relation to P_{s} X. Explicitly, for a representable yC, an ideal X := \underrightarrow{lim}_{i} yC_{i} and an object D of the base category:

ϵ_{yC} (D) := {⟨f, S⟩ ∈ yC(D) × P_{s} (yC)(D)|Γ(f) ≤ S}, and
ϵ_{X} := \underrightarrow{lim}_{i} ϵ_{yC_{i}} .

4.12. P_{s} is an Ideal.

4.13. Lemma. If R is a pretopos and C is an object of R, then the purported powerobject presheaf P_{s} (yC) := Sub_{R}(− × C) is a sheaf.

Proof. Notice that P_{s} (yC)(0) ≅ {∗} and, since coproducts in R are stable, P_{s} (yC)(A+ B) ≅ P_{s}(yC)(A)×P_{s}(yC)(B). Suppose f : A [figure] B is a cover and let h, k : Z [figure] Sub_{R}(B× C) be given such that Sub_{R}(f × C) ∘ h = Sub_{R}(f × C) ∘ k. Then, for any z ∈ Z, h(z), k(z) ∈ Sub_{R}(B × C) and the pullback P of h(z) along f × 1_{C} is also the pullback of k(z) along f × 1_{C}. But covers are preserved under pullback in R so that h(z) = k(z) by the uniqueness of image factorizations.

4.14. Proposition. If R is a Heyting pretopos and C is an object of R, then the purported small powerobject P_{s} (yC) is an ideal.

Proof. Since R is effective it suffices to show that P_{s} (yC) is separated. To that end let yD [figure] P_{s} (yC) × P_{s} (yC) be given and consider the following diagram:

[figure: P_{s} (yC); P_{s} (yC) × P_{s} (yC); Δ; yD; P_{s} (yC) × P_{s} (yC); i; P_{s} (yC) × P_{s} (yC); P_{s} (yC); π_{1}; P_{s} (yC) × P_{s} (yC); P_{s} (yC); π_{2}]

We will show that the equalizer of π_{1} ∘ i and π_{2} ∘ i is representable.

By the Yoneda lemma there are subobjects α, β ∈ Sub_{R}(D × C) corresponding to π_{1} ∘ i and π_{2} ∘ i, respectively. We want to find some H and h : H [figure] D in R such that the result of pulling α back along h × 1_{C} is the same as the result of pulling β back along h × 1_{C}.

[figure: H × C; D × C; h×1_{C}; ·; H × C; ·; α; α; D × C]

Define subobjects G and H of D × C and D, respectively, as follows:

G := [[x, y|α(x, y) ⇔ β(x, y)]],

and:

H := ∀_{π_{D}}(G)
= [[x|(∀z)(α(x, z) ⇔ β(x, z))]],

where π_{D} is the projection D × C [figure] D. Finally, let h : H [figure] D.

To see that α and β both pull back to the same thing along h × 1_{C} notice that, where ᾱ is the pullback of α along h × 1_{C} and β̄ is similarly defined:

ᾱ = [[x, y|α(x, y) ∧ (∀z)(α(x, z) ⇔ β(x, z))]]
= [[x, y|β(x, y) ∧ (∀z)(α(x, z) ⇔ β(x, z))]]
= β̄.

So, π_{1} ∘ i ∘ yh = π_{2} ∘ i ∘ yh.

To see that yH is the equalizer suppose given some η : X [figure] yD with π_{1}∘i∘η = π_{2}∘i∘η. It suffices to assume that X is representable, so suppose X ≅ yE. Consider the image factorization yE′ of η:

[figure: yE; yD; η; yE; yE′; ye′; yE′; yD; ye]

Notice that π_{1} ∘ i ∘ ye = π_{2} ∘ i ∘ ye since ye′ is a cover. That is, it suffices to consider monomorphisms m into yD with π_{1} ∘ i ∘ m = π_{2} ∘ i ∘ m. In particular, if α and β pull back to the same thing along η × 1_{C}, then they already are the same when pulled back along e × 1_{C}. Let ϵ denote the result of pulling α, β back along e × 1_{C}.

We will now show that E′ [figure: e] D factors through H [figure: h] D in R. Note that:

E′ ≤ H in Sub_{R}(D) iff π_{D}^{∗}(E′) ≤ G in Sub_{R}(D × C),
iff π_{D}^{∗}(E′) ≤ α ⇒ β and ≤ β ⇒ α,
iff α ∧ π_{D}^{∗}(E′) ≤ β and β ∧ π_{D}^{∗}(E′) ≤ α.

But α ∧ π_{D}^{∗}(E′) = ϵ = β ∧ π_{D}^{∗}(E′) is ≤ α and ≤ β by definition.

So there exists a map ē : E′ [figure] H such that h ∘ ē = e. To show ē ∘ e′ is the unique map from E making η factor through H suppose that f : E [figure] H and h ∘ f = η. By the uniqueness of image factorizations it follows that f = ē ∘ e′.

4.15. Lemma. The functor Sub_{R}^{r} : R [figure] Idl(R) defined by Sub_{R}^{r}(C) := Sub_{R}(− × C) preserves monomorphisms.

Proof. A map f : D [figure] C induces a natural transformation φ : Sub_{R}(−×D) [figure] Sub_{R}(−× C) given at an object E of R by:

S ∈ Sub_{R}(E × D) [figure: φ_{E}] S′ ∈ Sub_{R}(E × C), where
S′ := (1_{E} × f)_{!}(S).

As such, we define Sub_{R}^{r}(f) := φ. Notice that φ is natural since R satisfies the Beck-Chevalley condition.

If f is monic, then each component φ_{E} is monic and, by the Yoneda lemma, φ is monic (since the monomorphisms, like other limits, in Idl(R) agree with those in R̂).

4.16. Definition. For any object X = \underrightarrow{lim}_{i} yC_{i} of Idl(R), where R is a Heyting pretopos, we have by Proposition 4.5 and the foregoing lemma that there is a unique functor P_{s} : Idl(R) [figure] Idl(R) with:

P_{s} (X) ≅ P_{s} (\underrightarrow{lim}_{i} yC_{i})
≅ \underrightarrow{lim}_{i} Sub_{R}^{r}(C_{i})
= \underrightarrow{lim}_{i} Sub_{R}(− × C_{i}).

4.17. P_{s} (X) is a Powerobject. We will now show that the axiom (P1) holds in Idl(R) where R is a Heyting pretopos. It will be more efficient to break the proof into several steps. Also, notice that we write ∈_{X} for the membership relation in R̂ and ϵ_{X} for the membership relation in Idl(R). Similarly, we write PX for the power object in R̂ and P_{s} X for the small power object in Idl(R).

4.18. Lemma. Given any small relation R [figure: r] X × Y in Idl(R) there exists a unique classifying map r̂: Y [figure] P_{s} X.

Proof. First consider the case where R [figure] yC × yD. Then in R̂ both of the following squares (and the outer rectangle):

[figure: yC × P_{s} yC; yC × PyC; 1×i; ϵ_{yC}; yC × P_{s} yC; ϵ_{yC}; ∈_{yC}; ∈_{yC}; yC × PyC; P_{s} yC; PyC; i; yC × P_{s} yC; P_{s} yC; yC × P_{s} yC; yC × PyC; yC × PyC; PyC]

are pullbacks where ∈_{yC} and PyC are the presheaf membership and powerobject relations and i is the inclusion of P_{s} yC into PyC (P_{s} yC is, by definition, a subfunctor of P_{s} yC).

Notice that R is representable since r is a small relation. In particular, R = yE for some object E of R and r = ye. So, using the ‘twist’ isomorphism ˜ : C × D ≅ D × C, we have a relation ẽ: E [figure] D × C. By the Yoneda lemma such an element corresponds to a map r̂: yD [figure] P_{s} yC.

We will now show that the canonical classifying map ρ : yD [figure] PyC in R̂ factors through r̂. I.e., we show that:

[figure: yD; PyC; ρ; yD; P_{s} yC; r̂; P_{s} yC; PyC; i]

commutes. Notice that, by the two pullbacks lemma, this will suffice to show that r̂ is a classifying map for R in Idl(R). By the proof of the Yoneda lemma the action of r̂ on a given member f of yD(F) is:

[figure: f; P_{s} (yC)(f)(ẽ).]

But, ρ_{F} (f) = (yf × 1_{yC})^{∗}(yẽ) = i(P_{s} (yC)(f)(ẽ)).

For uniqueness suppose that q : yD [figure] P_{s} yC such that:

[figure: yC × yD; yC × P_{s} yC; 1×q; yE; yC × yD; yE; ϵ_{yC}; ϵ_{yC}; yC × P_{s} yC]

is a pullback. Then, in R̂, ye is the pullback of ∈_{yC} along i ∘ q and along i ∘ r̂ = ρ. Since ρ is unique with this property it follows that i ∘ r̂ = i ∘ q and, since i is monic, q = r̂.

Now, for any ideal X ≅ \underrightarrow{lim}_{i} yC_{i} and small relation r : R [figure] X × yD, R must be representable since the projection:

R [figure] X × yD [figure] yD

is small. I.e., R ≅ yE for some E. By Representable Compactness 4.3 there exists then a factorization of r:

R [figure] yC_{i} × yD [figure] X × yD

for some i. Thus indeed SRel_{X} ≅ \underrightarrow{lim}_{i} SRel_{yC_{i}}.

4.19. Lemma. For any ideal X, ϵ_{X} [figure] X × P_{s} X is a small relation.

Proof. It clearly suffices to verify this for the case where X is a representable yC. Let yD [figure] P_{s} yC be given. Then there is a r : R [figure] C × D in R such that:

[figure: ϵ_{yC}; P_{s} yC; π_{yC}; yR; ϵ_{yC}; yR; yD; π∘yr; yD; P_{s} yC]

is a pullback, as required.

4.20. Corollary. Any relation R [figure] X ×Y such that there exists a unique classifying map ρ : Y [figure] P_{s} X is a small relation.

Proof. By (S2) and the fact that ϵ_{X} is a small relation.

Putting the foregoing together we have the following proposition:

4.21. Proposition. If R is a Heyting pretopos and X ≅ \underrightarrow{lim}_{i} yC_{i} is an object of Idl(R), then P_{s} (X) = \underrightarrow{lim}_{i} Sub_{R}(− × C_{i}) is a small powerobject.

Moreover, when combined with the fact that axioms (S1)-(S5) are satisfied in pretopoi we have shown the following:

4.22. Theorem. If R is a Heyting pretopos, then Idl(R) is a category with basic class structure.

4.23. Remark. It should be mentioned that Alex Simpson was the first to give a proof of Proposition 4.14 (the main difference between his proof and the one given in this paper is our use of the Joyal Condition).

4.24. Exponentiation. We now extend the results of the preceding subsection by showing that if R is a Π-pretopos, then Idl(R) satisfies (E). First we need the following beautiful and useful fact:

4.25. Proposition. If C is a small category and P is an object of Idl(C), then:

Idl(C)/P ≃ Idl(∫_{C} P).

Proof. Here ∫_{C} P denotes the category of elements of P as in [Mac Lane and Moerdijk, 1992]. It is well known that Ĉ/P ≃ ˆ∫_{C} P. In particular, there are two functors R : Ĉ/P [figure] ˆ∫_{C} P and L : ˆ∫_{C} P [figure] Ĉ/P such that L ⊣ R and the two maps are pseudo-inverse to one another. These functors are defined as follows:

• R(η : F [figure] P) is a functor given by:

(c, C) [figure] Hom_{Ĉ/P} (c̃: yC [figure] P, η : F [figure] P),

where c̃ is the map in Ĉ corresponding to the element c ∈ P (C) by the Yoneda lemma.

• L(F) := \underrightarrow{lim}_{J} π ∘ i where J := ∫_{∫_{C} P}, i : ∫_{C} P [figure] Ĉ/P is the map taking an object (c, C) to the corresponding c̃: yC [figure] P as above and π is the projection from the category of elements.

We begin by showing that if (η : F [figure] P) is an object of Idl(C)/P, then R(P) is isomorphic to an object of Idl(∫_{C} P). Let η be given as mentioned. Then, since F is an ideal we have F ≅ \underrightarrow{lim}_{I} yD_{i} with maps μ_{i} : yD_{i} [figure] F making up the cocone.

We define a functor G : I [figure]∫_{C} P such that \underrightarrow{lim}_{I} yG_{i} ≅ R(η) and \underrightarrow{lim}_{I} yG_{i} is an object of Idl(∫_{C} P). Let G(i) := { \atop η ∘ μ_{i}} be the object corresponding via the Yoneda lemma to η ∘ μ_{i}. Given f : i [figure] j in I, let G(f) := D(f). G is easily seen to be functorial.

Next, let T := \underrightarrow{lim}_{I} yG. We now define an isomorphism φ : R(η) [figure] T. If f ∈ R(η)(c, C) then we have f : yC [figure] F. But using Representable Compactness there exists an i together with a map yl : yC [figure] yD_{i} such that μ_{i} ∘yl = f. Now, an element of T (c, C) is an equivalence class [g : C [figure] D_{i}]_{∼} where g : C [figure] D_{i} ∼ g′ : C [figure] D_{i′} if and only if there exists an object i′′ of I together with maps h : i [figure] i′′ and h′ : i′ [figure] i′′ such that D(h) ∘ g = D(h′) ∘ g′. So we define φ_{(c,C)}(f) := [l]_{∼}. The naturality of φ follows from the fact that I is filtered and the maps μ_{k} : yD_{k} [figure] F are monic.

Now we need an inverse map ψ : T [figure] R(η). If [g : C [figure] D_{i}]_{∼} ∈ T (c, C), then let ψ_{(c,C)}([g]_{∼}) := μ_{i} ∘ yg. This definition is independent of choice of representative by the fact that I is filtered and naturality is straightforward.

Finally, it is straightforward to verify, using the fact that I is filtered, that φ∘ψ = 1_{T}. Moreover, ψ ∘ φ = 1_{R(η)} is trivial. Furthermore, G is easily seen to preserve monomorphisms. As such, we have shown that R(η) is an ideal in Idl(∫_{C} P).

Similarly, given an object F of Idl(∫_{C} P) it follows from the fact that π : ∫_{∫_{C} P} F [figure] ∫_{C} P

and i : ∫_{C} P [figure] Ĉ/P both preserve monomorphisms that L(F) is an object of Idl(C)/P.

4.26. Proposition. If R is a Π-pretopos, then Idl(R) satisfies (E).

Proof. First, we show that given !_{yC} : yC [figure] 1 and f : X [figure] yC the map Π_{!_{yC}}(f) [figure] 1 is small. By definition we have the following pullback square:

[figure: 1; yC^{yC}; π̃_{yC}; Π_{!_{yC}}(f); 1; Π_{!_{yC}}(f); X^{yC}; X^{yC}; yC^{yC}; f^{yC}]

where π̃_{yC} is the transpose of 1_{yC}. However, since f is small it follows that X is representable. I.e., X ≅ yE for some E. But since R is a Π-pretopos it follows that:

yC^{yC} ≅ y(C^{C}), and
yE^{yC} ≅ y(E^{C}).

Therefore f^{yC} is a small map and by (S2) so is the map π_{!_{yC}}(f) [figure] 1.

The general case then follows from the foregoing proposition.

4.27. Universes and Infinity. If R is a Heyting pretopos, then we may construct universes U in Idl(R) as fixed points for endofunctors (cf. [Rummelhoff, 2004] or [Awodey and Forssell, 2004]). Given such a universe U in Idl(R), the full subcategory ↓(U) of Idl(R) consisting of those objects X of Idl(R) which are subobjects of U is a category of classes with U as the universal object (cf. [Simpson, 1999]). Putting this fact together with the results of the foregoing subsections we have our main theorem:

4.28. Theorem. If R is a Heyting pretopos, then there exists a universe U in Idl(R) such that ↓(U) is a basic category of classes in which R is equivalent to the category of small objects:

R ≃ S_{Idl(R)}.

Moreover, if R is a Π-pretopos, then ↓(U) is a predicative category of classes.

Proof. Let A := ∐_{C∈R} yC and U a fixed point of F (X) = A + P_{s} (X):

U ≅ A + P_{s} (U).

Cf. [Awodey and Forssell, 2004].

The reader should note that such initial models will satisfy the Simple Sethood axiom and, as such, Δ_{0}-separation.

One may also be interested in providing ideal models of set theories satisfying Infinity∗. Such models are obtained by adding a natural number object to the base category:

4.29. Corollary. If R is a Heyting pretopos with a natural number object, then:

(↓(U), U) ⊧ Infinity*.

However, there is an additional question as to how (and whether) one may obtain ideals models of stronger induction principles such as induction for classes as well as sets. This is an issue of considerable interest, but is one which we will not take up here.

4.30. Collection and Ideal Completeness. Ideal categories actually have some additional properties which are worth briefly mentioning.

4.31. Definition. A category with basic class structure is saturated if and only if it satisfies the following:

Small covers: Given a cover e : E [figure] D such that D is a small object, there exists a small subobject m : E′ [figure] E such that e ∘ m is a cover.

Small generators: If every small subobject m : D [figure] E factors through some l : E′ [figure] E, then E′ ≅ E.

Saturated categories with (impredicative) class structure were considered by Awodey et al [Awodey et al, 2004] in connection with their (inclusion) ideal models (see above) of the set theory BIST. We will employ them to prove an analogous result for predicative theories.

4.32. Lemma. If R is a Heyting pretopos, then Idl(R) is saturated.

Proof. Since the representable functors generate Idl(R) the second condition is easily seen to hold. For small covers, let a cover φ : X [figure] yC be given with X ≅ \underrightarrow{lim}_{i} yD_{i}. We employ the description of covers in Idl(R) as those maps which are locally epimorphic. Applying the criteria for locally epimorphic maps to φ, C, and 1_{C} we have that there exists a covering family (f_{k} : E_{k} [figure] C)_{k∈K} where K is finite such that, for all k ∈ K, f_{k} ∈ im(φ_{E_{k}}). Let E := ∐_{k} E_{k} and p : E [figure] C.

So, yp : yE [figure] yC. Moreover, for all k ∈ K, yf_{k} : yE_{k} [figure] yC factors through φ via the map ξ_{f_{k}} corresponding to x_{f_{k}} under the Yoneda lemma. Since yE is a coproduct it follows that there exists a unique map μ : yE [figure] X such that, for each coproduct injection l_{k} : E_{k} [figure] E, μ ∘ yl_{k} = ξ_{f_{k}}. As such, φ ∘ μ = yp. By definition X ≅ \underrightarrow{lim}_{i} yD_{i}. Therefore, by representable compactness, μ factors through some yh_{i} : yD_{k} [figure] X via a map μ̄ : yE [figure] yD_{i}. But then φ ∘ yh_{i} ∘ μ̄ = yp and φ ∘ yh_{i} is a cover, as required.

Small covers implies that the ideal models will satisfy, in addition to the other axioms of BCST (or CST if R is a Π-pretopos), the Strong Collection axiom. First, another axiom in which we will be interested is the (categorical) strong collection axiom [Joyal and Moerdijk, 1995]:

4.33. Definition. A system S of small maps in a category C with pullbacks is said to have collection if and only if it satisfies the following axiom:

(S6) For any cover p : D [figure] C and f : C [figure] A in S there exists a quasi-pullback square:

[figure: A′; A; h; A′; C′; f′; C′; D; D; C; p; A; C; f]

such that h is a cover and f′ is in S.

4.34. Proposition. [Typed Strong Collection] If a category C with basic class structure satisfies (S6), then:

C ⊨ ∀a : P_{s} C.(∀x ϵ_{C} a.∃y : D.φ(x, y) ⇒ ∃b : P_{s} D.coll(x ϵ_{C} a, y ϵ_{D} b, φ(x, y)),

where φ is any relation on C × D.

Proof. A routine but fairly lengthy exercise in the internal language.

4.35. Proposition. If C is a category with basic class structure that has small covers, then C satisfies (S6).

Proof. By Theorem 3.17, it suffices to show consider the case where we are given a cover e : E [figure] C with !_{C} : C [figure] 1 a small map. By (2) there exists a small subobject m : B [figure] E and the following is easily seen to be a quasi-pullback:

[figure: 1; 1; 1; 1; B; B; E; E; C; e; 1; C]

Using the foregoing facts (and results of the previous sections) we have:

4.36. Proposition. For any Heyting pretopos R:

(↓(U), U) ⊧ Strong Collection.

Awodey et al [Awodey et al, 2004] have obtained, for the impredicative set theory BIST_{C} (BIST augmented with Strong Collection), a strengthening of the completeness result with respect to models in (impredicative) categories of classes with collection. This so-called ‘topos-completeness’ result may be replicated for impredicative set theories as well, and we will now summarize this construction. In the statement of the following theorems we will state everything for BCST exclusively. However, all of the results are obtained for CST in the exact same way.

4.37. Lemma. BCST_{C} is complete with respect to models in basic categories of classes which have collection.

Proof. Cf. [Awodey et al, 2004].

4.38. Lemma. For any basic category of classes C with collection there exists a basic category of classes C′ which has collection and is saturated and a functor F : C [figure] C′ which is conservative and logical.

Proof. The proof from [Awodey et al, 2004] does not use any impredicative features of the starting category C.

4.39. Remark. The proof of 4.38 requires some form of the axiom of choice. However, it is not entirely clear to the author whether the full (non-constructive) strength of choice is required or whether a similar proof may be given in a predicative meta-theory (as codified by, say, CZF augmented with the axiom of multiple choice).

4.40. Lemma. If a basic category of classes C is saturated, then there is a conservative logical functor d : C [figure] Idl(S_{C}), namely, the restricted Yoneda embedding:

d(C) := Hom_{C}(i−, C),

where i : S_{C} [figure] C is the inclusion functor.

Assembling the pieces as in [Awodey et al, 2004] give the following result which says that BCST_{C} is complete with respect to models over Heyting pretopoi.

4.41. Theorem. For any formula φ of BCST_{C}, if, for all Heyting pretopoi R, (↓(U), U) ⊧ φ, then BCST_{C} ⊢ φ.

Proof. Again, the proof contained in [Awodey et al, 2004] requires no impredicative means.

References

P. Aczel and M. Rathjen, Notes on constructive set theory. Institut Mittag-Leffler (Royal Swedish Academy of Sciences) technical report number 40, 2001. Available at

    http://www.ml.kva.se/preprints/archive2000-2001.php.

S. Awodey, C. Butz, A. Simpson and T. Streicher, Relating set theories, toposes and categories of classes. In preparation, 2004. A preliminary version is available from the

    AST website http://www.phil.cmu.edu/projects/ast/ as CMU technical report

CMU-PHIL-146, June 2003.

S. Awodey and H. Forssell, Algebraic models of intuitionistic theories of sets and classes. Carnegie Mellon University technical report CMU-PHIL-156, July 2004.

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

N. Gambino, Presheaf models of constructive set theories. Submitted for publication, 2004.

B. Jacobs, Categorical Logic and Type Theory. Elsevier, Amsterdam, 1999.

P. T. Johnstone, Sketches of an Elephant volume 2. Oxford University Press, Oxford, 2003.

A. Joyal and I. Moerdijk, Algebraic Set Theory. Cambridge University Press, Cambridge, 1995.

S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic. Springer-Verlag, Berlin, 1992.

I. Moerdijk and E. Palmgren, Wellfounded trees in categories. Annals of Pure and Applied Logic, 104:189-218, 2000.

I. Moerdijk and E. Palmgren, Type theories, toposes and constructive set theory: Predicative aspects of AST. Annals of Pure and Applied Logic, 114:155-201, 2002.

I. Rummelhoff, Algebraic Set Theory. PhD thesis, University of Oslo, 2004. Forthcoming.

D. Scott, Lambda calculus: some models, some philosophy. In J. Barwise, H. J. Keisler and K. Kunen, editors, The Kleene Symposium, pages 381-421. North-Holland, Amsterdam, 1980.

D. Scott, Category-theoretic models for intuitionistic set theory. Manuscript slides of a talk given at Carnegie Mellon University (additions made in September 1998), December 1985.

A. Simpson, Constructive set theories and their category-theoretic models. Draft, 2004.

A. K. Simpson, Elementary axioms for categories of classes. Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 77-85, 1999.

M. A. Warren, Predicative categories of classes. Master’s thesis, Carnegie Mellon University, 2004.

Department of Philosophy, Carnegie Mellon University 135 Baker Hall, 5000 Forbes Ave., Pittsburgh, PA, USA 15213.

Email: awodey@andrew.cmu.edu
      mwarren@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/1/15-01.{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}TEX2e 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