0

d1

d

(f) (g) (h)

In the case of the Grothendieck construction, (f) says that ¼1 preserves composi-

tion and (g) and (h) say that the composite has the correct source and target.

As we have presented these diagrams, we have observed that they are all

true in the case of the Grothendieck construction in Set. In the case of the

Grothendieck construction,

(D0; D1 ; source; target; unit; comp)

is actually a category, hence a category object in Set. Moreover, ¼ = (¼0 ; ¼1 ) is

a functor, namely G(F ). That is actually true in any category, as seen in the

following.

Let

5.7.4 Proposition

(D0; D1 ; D2; d 0 ; d 1 ; u; ¼0 ; ¼1; p1 ; p2 ; c)

be an external functor to a category object

= (C0; C1 ; source; target; unit; comp)

5.8 The realizability topos 79

in a category . Then

(D0; D1 ; source; target; unit; comp)

is a category object in and (¼0; ¼1 ) is a functor in .

The proof is a lengthy series of diagram chases.

The converse is true, too: up to some technicalities, an external functor in Set

arises from a functor to Set from a small category. That means we said enough

about it in E{1 through E{4 to characterize it.

5.7.5 Theorem Let

0

; d 1 ; u; ¼0 ; ¼1; p1 ; p2 ; c)

( 0; 1; 2; d

be an external functor to a category

=( 1 ; source; target; unit; comp)

0;

¡ Set by

!

in Set. De¯ne F :

¡1

F{1 If C is an object of , then F (C) = ¼1 (C).

F{2 If f : C ¡ C 0 is an arrow of

! and x 2 F (C), then F (f )(x) is the target

for which ¼1(®) = f and d 0 (®) = x.

of the unique arrow ® of

¡ Set is a functor, and there is a unique isomorphism ¯ :

! ¡

!

Then F :

G( ; F ) for which G(F ) ± ¯ = ¼.

This theorem is essentially the discrete case of Theorem ES 4.3.7.

F{2 makes use of the fact that Diagram (ES 5.4)(a) is a pullback. A seasoned

categorist will simply name ® 2 F 2 as (x; f ), since he knows that between any

two pullbacks de¯ned by (ES 5.4)(a) there is a unique isomorphism respecting

the projections ¼1 and d 0 .

5.8 The realizability topos

The category of modest sets has been proposed as a suitable model for the poly-

morphic ¸-calculus. It is a subcategory of a speci¯c topos, the realizability topos.

Space limitations prevent us from giving a full exposition of this topic, Here we

describe how the realizability topos and the subcategory of modest sets are con-

structed. Further references are [Carboni, Freyd and Scedrov, 1988], [Rosolini,

1990], [Gray, 1991].

80 Toposes

5.8.1 Realizability sets In the discussion below, we will be writing f (x)

where f is a partial function. It will be understood that f (x) is de¯ned when

we write this.

A realizability set is a pair A = (A; =A ) where A is a set called the carrier

of A and =A : A £ A ¡ ! (N ) is a function to sets of natural numbers (thought of

as reasons that two elements are equal; in fact, they can be thought of as the set

of G„del numbers of proofs that they are). We denote the value of this function

o

at (a1 ; a2) 2 A £ A by [[a1 =A a2 ]], often abbreviated to [[a1 = a2 ]]. This is subject

to the following conditions:

REAL{1 There is a partial recursive function f such that for any a1, a2 2 A and

n 2 [[a1 = a2 ]], f (n) 2 [[a2 = a1 ]].

REAL{2 There is a partial recursive function of two variables g with the property

that if n 2 [[a1 = a2 ]] and m 2 [[a2 = a3 ]], then g(n; m) 2 [[a1 = a3]].

This is made into a category by de¯ning an arrow from A = (A; =A ) to B =

(B; =B ) to be an equivalence class of partial functions Á : A ¡ B such that there

!

is a partial recursive function f such that n 2 [[a1 = a2 ]] implies that f (n) 2

[[Áa1 = Áa2 ]]. Two such arrows Á and Ã are equal if there is a partial recursive f

such that n 2 [[a = a]] implies that f (n) 2 [[Áa = Ãa]].

Note that the last de¯nition implies that f is de¯ned on all elements a 2 A

for which [[a = a]] 6;. The other elements of A are irrelevant.

=

5.8.2 This category is a topos. We will not prove this, but simply describe some

of the constructions required. To ¯nd products, for example, ¯rst choose a recur-

sive bijection f : N £ N ¡ N. If A = (A; =A) and B = (B; =B ) are realizability

!

sets, the product is (A £ B; =A £ =B), where the latter is de¯ned by

[[(a1 ; b1 ) = (a2 ; b2 )]] = ff(n; m) j n 2 [[a1 = a2 ]]; m 2 [[b1 = b2 ]]g

Notice that a choice of f is required to show that products exist. The products

thereby exist, but, owing to the uniqueness of categorical products, do not depend

in any way on the choice of the function.

Equalizers can be de¯ned as follows. If Á; Ã : A ¡ B are two arrows their

!

equalizer is given by (A; =Á;Ã ) where [[a1 =Á;Ã a2]] = [[Áa1 = Ãa2 ]].

Finally power objects can be constructed as follows. Let f denote a pairing

as above and also choose an enumeration ge of all the partial recursive functions.

The carrier of A is [A ¡ ! N], all functions from A to sets of natural numbers.

If P and Q are two such functions, then we will say that f(d; e) 2 [[P = Q]] if for

all n 2 P (a) and m 2 [[a = b]], we have gd (f (n; m)) 2 Q(b) and for all n 2 Q(a)

and m 2 [[a = b]], we have ge (f (n; m)) 2 P (b).

This topos is called the realizability or e®ective topos. It is due to Martin

Hyland [1982], although the basic idea goes back to S. Kleene. See also [Rosolini,

1987].

5.8 The realizability topos 81

5.8.3 Modest sets `Modest sets' is used more-or-less interchangeably to de-

note either a certain full subcategory of the category of realizability sets or an

internal category object of that topos. A great deal of e®ort has been put into

describing the connection between the two. We will begin with the former. The

category of modest sets can be described directly and then embedded into the

realizability topos.

A modest set consists of A = (N; =A ) where as usual N denotes the natural

numbers and =A is a partial equivalence relation or PER on N, which means

it is symmetric and transitive, but not necessarily re°exive. We think of A as a

quotient of a subobject of N; the subobject is the set of n for which n =A n

modulo the relation =A.

The category of modest sets has arrows from A to B de¯ned as partial recursive

functions f de¯ned on all n such that n =A n and such that n =A m implies that

f(n) =A f(m). Note that since the relation is symmetric and transitive, as soon

as there is some m with n =A m, it is also the case that n =A n and so f(n) and

f(m) are de¯ned.

The modest sets form a cartesian closed category. Choose, as above, an enu-

meration ge of the partial recursive functions. Then [A ¡ B] is the PER with re-

!

lation given by d =[A¡!B] e if and only if whenever n =A m then gd (n) =B ge (m).

The modest sets do not form a topos.

We embed the modest sets into the realizability sets by choosing a pairing f

and associating to the modest set A = (N; =A) the realizability set with carrier N

and e 2 [[n = m]] if and only if n =A m and e = f (n; m). Although this appears

to depend on the choice of a pairing, it is easy to see that up to isomorphism it