Return to Revisions

To the best of my knowledge, this has never been "officially" described in the set theoretic literature. This has been described by Blass and Scedrov in Freyd's models for the independence of the axiom of choice (Mem. Amer. Math. Soc. 79, 1989). (It is of course implicit and sometimes explicit in the topoi literature, for example Mac Lane and Moerdijk do a fair bit of the translation in Sheaves in Geometry and Logic.) There are certainly a handful of set theorists that are well aware of the generalization and its potential, but I've only seen a few instances of crossover. In my humble opinion, the lack of such crossovers is a serious problem (for both parties). To be fair, there are some important obstructions beyond the obvious linguistic differences. Foremost is the fact that classical set theory is very much a classical theory, which means that the double-negation topology on a site is, to a certain extent, the only one that makes sense for use classical set theory. On the other hand, although very important, the double-negation topology is not often a focal point in topos theory.