ñòð. 29 
In fact it cannot. The pairing is used only to show that products exist. But
their properties { in particular their isomorphism class { are independent of the
particular construction used to prove their existence. Similar remarks apply to
the cartesian closed structure, which does not depend on a particular enumeration
of the partial recursive functions.
5.8.4 The internal category of modest sets This is a very brief glance at
how one might internalize the description of modest sets to produce a category
object inside the category of realizability sets. Except by way of motivation,
this category object has no real connection with the category of modest sets.
Nevertheless, we will call it the internal category of modest sets.
This internal category has the remarkable property that every internal dia
gram in it has a limit. This is not possible for ordinary categories (unless they
are just posets), but the proof that it is not possible requires a property of set
theory which is not valid for the realizability sets (namely the axiom of choice).
The construction is an exercise in internal expression. A modest set is a re
lation on N with certain properties. The natural numbers object in the category
82 Toposes
of realizability sets is the object (N; =N ), where e 2 [[n =N m]] if and only if
n = m = e. That is [[n =N m]] = fng if n = m and is empty otherwise. We will
denote it by N. Then a modest set is a subset of N Â£ N with certain properties.
The set of objects of the internal category of modest sets is then a certain
set of subsets of N Â£ N, which is the same as a subset of (N Â£ N). We want
to describe this subset as consisting of those relations that are symmetric and
transitive and double negation closed. The trick is to deÂ¯ne endoarrows s and t of
(N Â£N) that associate to a relation R the relations R op and R Â± R, respectively.
For s, this is easy. There is an arrow hp2; p1 i : N Â£ N Â¡ N Â£ N that switches the
!
coordinates and we let s = (hp2; p1 i).
For t, it is a little harder. By Yoneda, an arrow (N Â£ N) to itself can be
deÂ¯ned by describing a natural transformation Hom(Â¡; (N Â£ N)) to itself. An
element of Hom(A; (N Â£ N)) is, by the deÂ¯ning property of , a subobject
R Âµ A Â£ N Â£ N. Given such an R, we deÂ¯ne R0 to be the pullback in the following
diagram:
R
R0
? ?
 AÂ£N
R
The two maps from R Â¡ A Â£ N are the inclusion into A Â£ N Â£ N followed by
!
hp1 ; p2i and hp1 ; p3i, respectively. You should think of R as being a set of triples
(a; n1 ; n2 ) and then R0 Âµ A Â£ N Â£ N Â£ N is the set of 4tuples (a; n1 ; n2; n3) such
that (a; n1 ; n2) 2 R and (a; n2 ; n3 ) 2 R. Then the inclusion of R 0 into AÂ£NÂ£NÂ£N
followed by hp1 ; p2 ; p4 i gives us an arrow R0 Â¡ A Â£ N Â£ N whose image we denote
!
by t(R). It is interpreted as the set of (a; n1; n3 ) such that there is an n2 with
both (a; n1; n2) 2 R and (a; n2; n3) 2 R. We omit the proof that this construction
from R to t(R) is natural in A, but assuming that, it follows from the Yoneda
Lemma that this results from an endomorphism t of (N Â£ N).
Finally, the object M0 of objects is deÂ¯ned as the limit of

s

(N Â£ N)  (N Â£ N)
t
where the middle arrow is the identity. This is to be interpreted as the set of
relations that are Â¯xed under both s and t.
The object M0 is the object of objects of the internal category of modest sets.
The object of arrows is deÂ¯ned as a subobject of the object [N Â¡ N]e of partial
!
arrows of N to N; namely those that satisfy the internal version of the deÂ¯nition
of the ordinary of modest sets. This construction is tedious, but not diÂ±cult, and
we omit it.
Answers to Exercises
Solutions for Chapter 1
Section 1.1
1. This should have two sorts 1 and b. There should be an operation true : 1 Â¡ b,
!
an operation false : 1 Â¡ b and a cocone
!
1 1
@ Â¡
true@ Â¡ false
@ Â¡
R
@ Â¡
Âª
b
We need a cone with empty base to express that 1 is terminal. We should have
operations _ : b Â£ b Â¡ b, ^ : b Â£ b Â¡ b and : : b Â¡ b. We will need diagrams to
! ! !
express equations like
: true = false
: false = true
: ^ (x; y) _(x; y)
=
_(0; 0) = 0
_(0; 1) = 1
_(1; 0) = 1
_(1; 1) = 1
There are other equations, but they all follow from these. In particular, we do
not, in this case, have to express the distributive laws since they follow, there
being so few elements.
2. If we have one sort 1, one empty cone with vertex 1 and one cocone
1 1
@ Â¡
id @ Â¡ id
@
R Â¡
Âª
1
83
84 Solutions for section 1.3
then there is no model in sets because the model must take 1 to the oneelement
set and that must satisfy that 1 = 1 + 1, which is impossible. It follows from
Exercise 4 of Section 8.6 that this sketch does have a model in the category of
monoids.
Section 1.2
1. This is most readily done using elements, although it can all be done with
diagrams. If x Â¤ xÂ¡1 = 1 and y Â¤ y Â¡1 = 1, then
(x Â¤ y) Â¤ (y Â¡1 Â¤ xÂ¡1) = x Â¤ (y Â¤ (y Â¤Â¡1 Â¤xÂ¡1 )) = x Â¤ ((y Â¤ y Â¡1 ) Â¤ xÂ¡1 )
= x Â¤ (1 Â¤ xÂ¡1 ) = x Â¤ xÂ¡1 = 1
If 2 60 in a Â¯eld, then 2Â¡1 exists, whence (2 Â¤ 2)Â¡1 = 4Â¡1 also exists. Hence 4 60.
= =
2. Let Q and F2 denote the Â¯elds of rational numbers and the twoelement Â¯eld
respectively. In order to have a product of Q and F2, we have to have a cone
F
Â¡ @
Â¡ @
Âª
Â¡ @
R
Q F2
which is exactly what we do not have in the category of Â¯elds.
Section 1.3
1. a. Several things have to be shown. First that the image N0 Âµ N is closed
under the operations (that is if all the arguments of the operation are in the
image, so does the value); second that the diagrams continue to commute; third
that the cones remain products; and fourth that the cocones remain sums.
Let u : s1 Â£ s2 Â£ Â¢ Â¢ Â¢ Â£ sn Â¡ s be an operation. For i = 1; : : : ; n let xi 2 M (si )
!
and x = u(x1 ; : : : ; xn ). Then f (x) = u(f (x1 ); : : : ; f (xn )), which demonstrates the
Â¯rst point. Since the operations in N0 are the restrictions of those in N any two
paths that agree on N do so on N0 (actually, whether or not they do on M ).
For the cones, we illustrate on binary cones. Suppose s Ãƒ r Â¡ t is a cone in the
Â¡!
sketch. Then in the diagram
 N0(r)   N (r)
ñòð. 29 