Editing History of topos theory (section)

==Position of topos theory==
There was some irony that in the pushing through of [[David Hilbert]]'s long-range programme a natural home for [[intuitionistic logic]]'s central ideas was found: Hilbert had detested the school of [[L. E. J. Brouwer]]. Existence as 'local' existence in the sheaf-theoretic sense, now going by the name of [[Kripke–Joyal semantics]], is a good match. On the other hand Brouwer's long efforts on 'species', as he called the intuitionistic theory of reals, are presumably in some way subsumed and deprived of status beyond the historical. There is a theory of the real numbers in each topos, and so no one master intuitionist theory.

The later work on [[étale cohomology]] has tended to suggest that the full, general topos theory isn't required. On the other hand, other sites are used, and the Grothendieck topos has taken its place within homological algebra.

The Lawvere programme was to write [[higher-order logic]] in terms of category theory. That this can be done cleanly is shown by the book treatment by [[Joachim Lambek]] and [[P. J. Scott]]. What results is essentially an intuitionistic (i.e. [[constructive logic]]) theory, its content being clarified by the existence of a ''free topos''. That is a set theory, in a broad sense, but also something belonging to the realm of pure [[syntax]]. The structure on its sub-object classifier is that of a [[Heyting algebra]]. To get a more classical set theory one can look at toposes in which it is moreover a [[Boolean algebra (structure)|Boolean algebra]], or specialising even further, at those with just two truth-values.  In that book, the talk is about [[Constructivism (mathematics)|constructive mathematics]]; but in fact this can be read as foundational [[computer science]] (which is not mentioned). If one wants to discuss set-theoretic operations, such as the formation of the image (range) of a function, a topos is guaranteed to be able to express this, entirely constructively.

It also produced a more accessible spin-off in [[pointless topology]], where the ''[[locale (mathematics)|locale]]'' concept isolates some insights found by treating ''topos'' as a significant development of ''topological space''. The slogan is 'points come later': this brings discussion full circle on this page. The point of view is written up in [[Peter Johnstone (mathematician)|Peter Johnstone]]'s ''Stone Spaces'', which has been called by a leader in the field of computer science 'a treatise on [[extensionality]]'. The extensional is treated in mathematics as ambient—it is not something about which mathematicians really expect to have a theory. Perhaps this is why topos theory has been treated as an oddity; it goes beyond what the traditionally geometric way of thinking allows. The needs of thoroughly intensional theories such as untyped [[lambda calculus]] have been met in [[denotational semantics]]. Topos theory has long looked like a possible 'master theory' in this area.