categories: Re: Subclassifier object question

[Paul Taylor <pt@dcs.qmw.ac.uk>]

Bill Halchin asks
> I don't understand how the notion of a subobject classifier
> determines whether "el" does or does not belong to the subobject

        U ----------> 1
        V  _|         |
        |             | true
        |             |
        V   chi       V
        X --------> Omega

If any element "belongs to U" in the arrows sense that it factors
through U, ie there is a map from 1 (or somewhere) to U, then the
composite with chi:X->Omega is equal to (the composite with) true.

Conversely, if an element of X "belongs to U" in the logical sense
that its composite with chi is equal to (the composite with)true, then
we have a commutative square that can be compared to the pullback.


For more about the logical consequences of this property of Omega,
and in particular the mysterious formula
      a & F(a)  =  a & F(true)
see "Geometric and Higher Order Logic ..." in TAC, v7 (2000) pp 284--338.

For a presentation of set theory (or, as I call it, Zermelo type theory)
in a form that is both the way that ordinary mathematicians use it,
and directly related to the topos-theoretic way of saying things,
see Section 2.2 of my book "Practical Foundations of Mathematics".

Both accessible via my home page at   http://www.dcs.qmw.ac.uk/~pt

Paul