{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T05:01:28Z","timestamp":1777525288137,"version":"3.51.4"},"reference-count":19,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":8685,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1990,6]]},"abstract":"<jats:p>The family of readability toposes, of which the effective topos is the best known, was discovered by Martin Hyland in the late 1970's. Since then these toposes have been used for several purposes. The effective topos itself was originally intended as a category in which various recursion-theoretic or effective constructions would live as natural parts of the higher-order type structure. For example the hereditary effective operators become the higher types over N (Hyland [1982]), and effective domains become the countably-based domains in the topos (McCarty [1984], Rosolini [1986]). However, following the discovery by Moggi and Hyland that it contained nontrivial small complete categories, the effective topos has also been used to provide natural models of polymorphic type theories, up to and including the theory of constructions (Hyland [1987], Hyland, Robinson and Rosolini [1987], Scedrov [1987], Bainbridge et al. [1987]).<\/jats:p><jats:p>Over the years there have also been several different constructions of the topos. The original approach, as in Hyland [1982], was to construct the topos by first giving a notion of P\u03c9-valued set. A P\u03c9-valued set is a set <jats:italic>X<\/jats:italic> together with a function =<jats:sub><jats:italic>x<\/jats:italic><\/jats:sub>: <jats:italic>X<\/jats:italic> \u00d7 <jats:italic>X<\/jats:italic> \u2192 P\u03c9. The elements of <jats:italic>X<\/jats:italic> are to be thought of as codes, or as expressions denoting elements of some \u201creal underlying\u201d set in the topos. Given a pair (<jats:italic>x<\/jats:italic>,<jats:italic>x<\/jats:italic>\u2032) of elements of <jats:italic>X<\/jats:italic>, the set =<jats:sub><jats:italic>x<\/jats:italic><\/jats:sub> (<jats:italic>x<\/jats:italic>,<jats:italic>x<\/jats:italic>\u2032) (generally written <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200026086_inline1\"\/>) is the set of codes of proofs that the element denoted by <jats:italic>x<\/jats:italic> is equal to the element denoted by <jats:italic>x<\/jats:italic>\u2032.<\/jats:p>","DOI":"10.2307\/2274658","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:35:29Z","timestamp":1146954929000},"page":"678-699","source":"Crossref","is-referenced-by-count":29,"title":["Colimit completions and the effective topos"],"prefix":"10.1017","volume":"55","author":[{"given":"Edmund","family":"Robinson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Rosolini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200026086_ref017","unstructured":"Scedrov A. [1987], HEO semantics for a calculus of constructions (to appear)."},{"key":"S0022481200026086_ref014","unstructured":"McCarty D. C. [1984], Realizability and recursive mathematics, D. Phil, thesis, Oxford University, Oxford."},{"key":"S0022481200026086_ref012","first-page":"109","volume":"10","author":"Kleene","year":"1945","journal-title":"On the interpretation of intuitionistic number theory"},{"key":"S0022481200026086_ref011","unstructured":"Hyland J. M. E. , Robinson E. P. and Rosolini G. [1987], The discrete objects in the effective topos (to appear)."},{"key":"S0022481200026086_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0022481200026086_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0022481200026086_ref009","volume-title":"Proceedings of the conference on Church's thesis: fifty years later","author":"Hyland","year":"1987"},{"key":"S0022481200026086_ref008","first-page":"165","volume-title":"The L. E. J. Brouwer centenary symposium","author":"Hyland","year":"1982"},{"key":"S0022481200026086_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-85844-4"},{"key":"S0022481200026086_ref006","volume-title":"The realizability universe","author":"Freyd","year":"1987"},{"key":"S0022481200026086_ref005","first-page":"23","volume-title":"Mathematical foundations of programming language semantics (proceedings, New Orleans, Louisiana, 1987","volume":"298","author":"Carboni","year":"1988"},{"key":"S0022481200026086_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/S1446788700018735"},{"key":"S0022481200026086_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058580"},{"key":"S0022481200026086_ref001","volume-title":"Logical foundations of functional programming (proceedings, Austin, Texas, 1987","author":"Bainbridge","year":"1987"},{"key":"S0022481200026086_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061839"},{"key":"S0022481200026086_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0022481200026086_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(82)90030-5"},{"key":"S0022481200026086_ref016","unstructured":"Rosolini G. [1986], Continuity and effectiveness in topoi, D. Phil, thesis, Oxford University, Oxford; published as Technical Report CMU-CS-86-123, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania."},{"key":"S0022481200026086_ref003","first-page":"10","volume":"50","author":"B\u00e9nabou","year":"1985","journal-title":"Foundations of category theory"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200026086","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,18]],"date-time":"2019-05-18T21:13:19Z","timestamp":1558213999000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200026086\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,6]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1990,6]]}},"alternative-id":["S0022481200026086"],"URL":"https:\/\/doi.org\/10.2307\/2274658","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,6]]}}}