FORCING AND CLASSIFYING TOPOI
of morphisms in E , natural in Z,Y „ Equivalently, for
each object X , the functor (-)*X: E •+ E has a right
adjoint (-)X: E + E .
(iii) E has a subobject classifier, i.e. an object ft and
a morphism 1 — * ft (called "true") such that, for each
monomorphism Y *- * X in E , there is a unique morphism
4 : X-*•ftin £ (the classifying map of a ) making
Y c *X
1 —^-* ft
a pullback diagram.
[Jo1 , §1.1] gives an outline of the proof that each presheaf category
S is an elementary topos.
A natural number object in an elementary topos E is an object N
together with morphisms 1 —*N—*N such that for any diagram
x u f
1 - * X - * X in E , there exists a unique N -» • X such that the following
;f ! f
In a presheaf topos S , the natural object is given by the con-
stant presheaf U .
In an elementary topos E , the lattice of subobjects of each object
is a Heyting algebra. If, in addition, for every A1-* B in E there is
A1 «-* B with AAA'= 0 , AvA' = B (so the lattice of subobjects of each
object of E is a Boolean algebra), we say that E is a Boolean topos.
0.4. Presheaf Semantics.
Any elementary topos interprets intuitionistic higher-order logic,
and any elementary topos with a natural number object interprets intuition-
istic higher-order arithmetic (Boolean topoi interpret classical logic)