William - Sorry, I was being stupid. The inverse image of a nonempty set may indeed be empty - it's the _image_ of a nonempty set that's always nonempty. This is obvious in retrospect but curious from a formal viewpoint because the inverse image is better-behaved in most ways: it preserves all meets and joins, while the image only preserves all joins, in general.

So yes, we need to discard the "empty parts" when forming the pullback of a partition. I'll fix the lecture. The deep meaning of this fact remains obscure to me.

So yes, we need to discard the "empty parts" when forming the pullback of a partition. I'll fix the lecture. The deep meaning of this fact remains obscure to me.