%0 Book Section %1 hyland1982effective %A Hyland, J.M.E. %B The L. E. J. Brouwer Centenary Symposium Proceedings of the Conference held in Noordwijkerhout %D 1982 %E Troelstra, A.S. %E van Dalen, D. %I Elsevier %K effective topos %P 165 - 216 %R http://dx.doi.org/10.1016/S0049-237X(09)70129-6 %T The Effective Topos %U http://www.sciencedirect.com/science/article/pii/S0049237X09701296 %V 110 %X Publisher Summary This chapter describes the most accessible of the series of toposes that can be constructed from notions of realizability: it is that based on the original notion of recursive realizability and presents the abstract approach to recursive realizability in some detail. The chapter introduces effective topos and discusses the notion of a negative formula that arises naturally in the theory of sheaves. The chapter presents features of effective topos, where the power-set matters: uniformity principles and properties of j-operators. The chapter recommends that while constructing a topos from a tripos, one must add new subobjects of the sets one has started with to represent the nonstandard predicates and take quotients of these by the nonstandard equivalence relations.

@incollection{hyland1982effective, abstract = {Publisher Summary This chapter describes the most accessible of the series of toposes that can be constructed from notions of realizability: it is that based on the original notion of recursive realizability and presents the abstract approach to recursive realizability in some detail. The chapter introduces effective topos and discusses the notion of a negative formula that arises naturally in the theory of sheaves. The chapter presents features of effective topos, where the power-set matters: uniformity principles and properties of j-operators. The chapter recommends that while constructing a topos from a tripos, one must add new subobjects of the sets one has started with to represent the nonstandard predicates and take quotients of these by the nonstandard equivalence relations. }, added-at = {2014-12-30T11:11:54.000+0100}, author = {Hyland, J.M.E.}, biburl = {https://www.bibsonomy.org/bibtex/2d01f04e8a88fa0e003e7b2e5f377ad9d/t.uemura}, booktitle = {The L. E. J. Brouwer Centenary Symposium Proceedings of the Conference held in Noordwijkerhout}, description = {The Effective Topos}, doi = {http://dx.doi.org/10.1016/S0049-237X(09)70129-6}, editor = {Troelstra, A.S. and van Dalen, D.}, interhash = {17e946b686e9aa824571006a4326b01b}, intrahash = {d01f04e8a88fa0e003e7b2e5f377ad9d}, issn = {0049-237X}, keywords = {effective topos}, pages = {165 - 216}, publisher = {Elsevier}, series = {Studies in Logic and the Foundations of Mathematics }, timestamp = {2014-12-30T11:11:54.000+0100}, title = {The Effective Topos }, url = {http://www.sciencedirect.com/science/article/pii/S0049237X09701296}, volume = 110, year = 1982 }