Categorification of spaces and models for set theory One aspect of topos theory is that it provides an enlarged view of the classical concept of space. Indeed, one may thought that the notion of topos is a sort of categorification of the notion of space. On the other hand, a topos can be thought as well as a model for set theory. 
Q: Is there some intuition underlying this (rather misterious) coincidence? I mean, why the categorical models for set theory should also provide the correct categorification for the notion of space?   
 A: Let me first recall an important lesson from category theory that morphisms in a category are more important than objects. When we think of toposes as generalized spaces we use geometric morphisms between them, but when we think of them as a universe of generalized sets morphisms are usually something different. What kind of morphisms we use in the latter case depends on what kind of internal language we use for our generalized sets. Often, it includes higher-order logic in which case we must use logical morphisms. This remark does not answer the question completely since we can forget about non-invertible morphisms between toposes and consider only the underlying 2-groupoid which is the same for geometric and logical morphisms. So, let me give another answer.
Since we are talking about logic, it is worth recalling that spaces (to be more precise, locales) are closely related to geometric logic. This paper is a nice overview of this relationship. The category of locales is equivalent to an appropriately defined category of propositional geometric theories. Similarly, Grothendieck toposes are equivalent to predicate geometric theories. Since the internal language of a Grothendieck topos supports not only geometric logic but also higher-order logic, we can think of it as a universe of generalized sets.
Finally, we can ask why it so happens that the internal language of a Grothendieck topos (defined as a classifying category of a geometric theory) supports higher-order logic. I don't have an answer to this question, but I can note that this also happens at the lower categorical level. Namely, frames happen to be Heyting algebras even though the existence of implications is not assumed explicitly.
A: IMHO the point of the question is not about the nature of categorification. In less controversial language, it would say "Why is 'the' category of generalized set theories also a category of generalized spaces?". (I will gloss over Valery Isaev's very good points about what the morphisms are here, and how they depend on what kind of logic one is interested in.) So basically there are two sides of the equation: generalizing spaces to toposes, and generalizing set theory to topos theory:


*

*For me, it's not so mysterious that the category of toposes can be regarded as a category of generalized spaces -- this basically just says that the category of sheaves remembers enough about a space that (sober) spaces embed fully faithfully into the category of toposes (and geometric morphisms). That's enough of a starting point to make it reasonable to generalize notions from topology to the study of arbitrary toposes, and to expect this perspective to be somewhat fruitful (and although I don't know that much about it, by impression is that this way of approaching the "elephant" of topos theory should always be supplemented by other perpsectives).

*So for me it's the other side of the equation which is more mysterious. That is, why is it that the main way we have of perturbing the notion of "set" is by passing to the notion of "set varying over a base"? To this I don't have a definitive answer. But I'll point out a few things:


*

*My understanding is that within set theory, there are basically two ways to build new models of set theory from old ones. One is to pass to inner models, and the other is via forcing. I think that inner models are like passing to certain subcategories of what one starts with -- I don't have a more detailed handle on what the categorical analog might be. But forcing really combines two constructions: first one passes to a category of sheaves, and then quotients by an ultrafilter on the poset over which the sheaves are defined. The ultrafilter quotient is really just there to keep the logic 2-valued, but the point is that passing to categories of sheaves is something that is already very important even if one is interested only in non-generalized sets. So the question might be reformulated (too sharply!) as "Why is forcing essentially the only method in set theory?".

*There is at least one other direction in which one can vary the notion of set -- one can drop cartesianness, and work with an arbitrary symmetric monoidal closed category (complete and cocomplete, say). There's a corresponding notion of logic, namely linear logic. I think most mathematicians would say that linear logic "feels" sufficiently different from ordinary logic that they'd rather think of these things on their own terms rather than trying to import every possible concept from set theory into this setting. One thing that puzzles me here is that I don't know if there is a good monoidal analog of local cartesian closure. I'm not sure how linear logicians deal with this. Absent that, I'm not sure it even makes sense to speculate on what kind of analogs of subobject classifiers might exist here.

*This reminds me of two papers: variation through enrichment and enrichment through variation; in the context of this discussion, the idea that variation over a base is a concept that might naturally arise from thinking about other things is enticing. I am feeling a bit too lazy at the moment to follow up and see if this is the kind of thing one finds there, but at any rate those are interesting papers which are worth reading. If I recall correctly, one of them works in a poset-enriched setting to simplify some coherence issues, and a generalization is to be found in Verity's thesis.
