Vaughan Pratt wrote:
My question to Steve and the list as a whole would be, if you had been assigned the task of writing an explanation section following the formal definition section, where would you have put the emphasis: on how the definition facilitates a first-order characterization of the notion of "subobject", or on the geometric morphism perspective?
Dear Vaughan, I would try to encapsulate what I said in "Locales and toposes as spaces". My aim there was to present ideas (of generalized space) that have been known to topos-theorists from the start, but which tend to get buried in the technical development. I wanted to show how results in Mac Lane and Moerdijk, or in the Elephant, can be read in a non-standard order to paint a particular picture. (To indulge myself in metaphors again, the blind toddler wanders right underneath, between the legs, feels nothing, and concludes the elephant is very like a generalized space. In its innocence, it never developed the respectful awe of the scary bits.) Some of the encapsulation is in my Linz lecture slides http://www.cs.bham.ac.uk/~sjv/LinzTalk.pdf My aim there was to explain how sheaves can be viewed as continuous set-valued maps, and what that tells us about continuity. In particular, I wanted to support the idea that "continuous" means "geometrically definable". This leads to the idea of geometric morphism between toposes as continuous map between generalized spaces. But then non-classical reasoning (no excluded middle, no axiom of choice, no impredicative constructions) enters in immediately as part of the geometricity. Best regards, Steve.