{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T07:08:00Z","timestamp":1749798480369},"reference-count":60,"publisher":"Elsevier","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1016\/b978-0-444-51621-3.50009-8","type":"book-chapter","created":{"date-parts":[[2012,4,21]],"date-time":"2012-04-21T15:43:50Z","timestamp":1335023030000},"page":"633-687","source":"Crossref","is-referenced-by-count":2,"title":["Types, Sets, and Categories"],"prefix":"10.1016","author":[{"given":"John L.","family":"Bell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0010","series-title":"Logic Colloquium '77","first-page":"55","article-title":"The type-theoretic interpretation of constructive set theory","author":"Aczel","year":"1978"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0015","series-title":"The L.E.J. Brouwer Centenary Symposium","first-page":"1","article-title":"The type-theoretic interpretation of constructive set theory: choice principles","author":"Aczel","year":"1982"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0020","series-title":"Logic, methodology and Philosophy of Science VII","first-page":"17","article-title":"The type-theoretic interpretation of constructive set theory: inductive definitions","author":"Aczel","year":"1986"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0025","series-title":"Types for Proofs and Programs vol. 2277 of Lecture Notes on Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-45842-5_1","article-title":"Collection principles in dependent type theory","author":"Aczel","year":"2002"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0030","series-title":"The generalized type-theoretic interpretation of constructive set theory","author":"Aczel","year":"2005"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0035","series-title":"Notes on Constructive Set Theory","author":"Aczel","year":"2001"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0040","series-title":"Toposes and Local Set Theories: An Introduction. Oxford Logic Guides 14","author":"Bell","year":"1988"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0045","series-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0050","series-title":"Types vs. Topos","author":"Boileau","year":"1975"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0055","doi-asserted-by":"crossref","first-page":"6","DOI":"10.2307\/2273251","article-title":"La logique de topos","volume":"46","author":"Boileau","year":"1981","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0060","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1023\/A:1004209106100","article-title":"Constructing Cantorian counterexamples","volume":"26","author":"Boolos","year":"1997","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0065","series-title":"Abriss der Logistik","author":"Carnap","year":"1929"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0070","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"1","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0075","series-title":"Theory of Constructive Types","author":"Chwistek","year":"1924"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0080","series-title":"Type Theory","author":"Coquand","year":"2006"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0085","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0090","series-title":"Categories for Types","author":"Crole","year":"1993"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0095","series-title":"North Holland","article-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0100","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1090\/S0002-9939-1975-0373893-X","article-title":"Axiom of choice and complementation","volume":"51","author":"Diaconescu","year":"1975","journal-title":"Proceedings of the American Mathematical Society"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0105","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1090\/S0002-9947-1945-0013131-6","article-title":"General theory of natural equivalences","volume":"58","author":"Eilenberg","year":"1945","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0110","series-title":"The Seven Virtues of Simple Type Theory","author":"Farmer","year":"2006"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0115","series-title":"Connections between category theory and logic","author":"Fourman","year":"1974"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0120","series-title":"Handbook of Mathematical Logic","first-page":"1053","article-title":"The logic of topoi","author":"Fourman","year":"1977"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0125","series-title":"Applications of Sheaves. Proc. L.M.S. Durham Symposium 1977","first-page":"753","year":"1979"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0130","series-title":"Logic Colloquium 76","first-page":"173","article-title":"The simple theory of types","author":"Gandy","year":"1977"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0135","series-title":"Interpr\u00e9tation fonctionelle \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure","author":"Girard","year":"1972"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0140","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF01700692","article-title":"\u00dcber formal untenscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatsh. Math. Phys."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0145","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1002\/malq.19780242514","article-title":"Choice implies excluded middle","volume":"24","author":"Goodman","year":"1978","journal-title":"Z. Math Logik Grundlag. Math."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0150","doi-asserted-by":"crossref","first-page":"323","DOI":"10.4064\/fm-52-3-323-344","article-title":"A theory of propositional types","volume":"52","author":"Henkin","year":"1963","journal-title":"Fund. Math."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0155","series-title":"To H. B. Curry: Essays on Combinatorial Logic. Lambda Calculus and Formalism","first-page":"479","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0160","series-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0165","series-title":"Topos Theory","author":"Johnstone","year":"1977"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0170","series-title":"Sketches of an Elephant:A Topos Theory Compendium, Vols. I and II. Oxford Logic Guides Vols. 43 and 44","author":"Johnstone","year":"2002"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0175","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0003-4843(74)90003-5","article-title":"Functional completeness of Cartesian categories","volume":"6","author":"Lambek","year":"1974","journal-title":"Annals of Mathematical Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0180","series-title":"To H.B. Curry:Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"375","article-title":"From \u03bb-calculus to Cartesian closed categories","author":"Lambek","year":"1980"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0185","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0001-8708(80)90013-4","article-title":"From types to sets","volume":"36","author":"Lambek","year":"1980","journal-title":"Adv. In Math."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0190","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/0022-4049(80)90102-4","article-title":"Intuitionist type theory and the free topos","volume":"19","author":"Lambek","year":"1980","journal-title":"Journal Pure and Applied Algebra"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0195","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/BF00253914","article-title":"Intuitionist type theory and foundations","volume":"10","author":"Lambek","year":"1981","journal-title":"Joural of Philosophical Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0200","series-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0205","series-title":"Quantifiers and sheaves. In Actes du Congr\u00e8s Intern. Des Math. Nice 1970, tome I","first-page":"329","author":"Lawvere","year":"1971"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0210","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BFb0073962","article-title":"Introduction to Toposes, Algebraic Geometry and Logic","volume":"274","author":"Lawvere","year":"1972","journal-title":"Springer Lecture notes in Math"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0215","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1017\/S0960129505004962","article-title":"Modular correspondence between dependent type theories and categories including pretopoi and topoi","volume":"15","author":"Maietti","year":"2005","journal-title":"Math. Struct. Comp. Sci."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0220","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1002\/malq.19990450410","article-title":"Can you add power-sets to Martin L\u00f6f's intuitionistic set theory?","volume":"45","author":"Maietti","year":"1999","journal-title":"Mathematical Logic Quarterly"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0225","series-title":"Logic Colloquium '73","first-page":"73","article-title":"An Intuitionistic theory of types; predicative part","author":"Martin-L\u00f6f","year":"1975"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0230","series-title":"Logic, Methodology and Philosophy of Science VI","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0235","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0240","series-title":"Computer Science Logic, Lecture Notes in Computer Science 2803","first-page":"441","article-title":"A strongly normalising Curry-Howard correspondence for IZF set theory","author":"Miquel","year":"2001"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0245","series-title":"Programming in Martin-L\u00f6f's Type Theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0250","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1112\/plms\/s2-25.1.338","article-title":"The foundations of mathematics","volume":"25","author":"Ramsey","year":"1926","journal-title":"Proceedings of the London Mathematical Society"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0255","series-title":"The Principles of Mathematics","author":"Russell","year":"1903"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0260","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","article-title":"Mathematical logic as based on the theory of types","volume":"30","author":"Russell","year":"1908","journal-title":"Am. J. Math."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0265","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0305004100061284","article-title":"Locally Cartesian closed categories and type theory","volume":"95","author":"Seely","year":"1984","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0270","doi-asserted-by":"crossref","first-page":"969","DOI":"10.2307\/2273831","article-title":"Categorical semantics for higher order polymorphic lambda calculus","volume":"52","author":"Seely","year":"1987","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0275","series-title":"Mathematics and Mind","first-page":"45","article-title":"The law of excluded middle and the axiom of choice","author":"Tait","year":"1994"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0280","doi-asserted-by":"crossref","first-page":"210","DOI":"10.4064\/fm-17-1-210-239","article-title":"Sur les ensembles definissable de nombres r\u00e9els I","volume":"17","author":"Tarski","year":"1931","journal-title":"Fundamenta Mathematicae"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0285","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879-1931","year":"1967"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0290","series-title":"Das Kontinuum","author":"Weyl","year":"1918"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0295","series-title":"Principia Mathematica","author":"Whitehead","year":"1910"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0300","series-title":"Local Set Theory and Topoi","author":"Zangwill","year":"1977"},{"key":"10.1016\/B978-0-444-51621-3.50009-8_bb0305","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF01449999","article-title":"Untersuchungen \u00fcber die Grundlagen der Mengenlehre I","volume":"59","author":"Zermelo","year":"1908","journal-title":"Matematische Annalen"}],"container-title":["Handbook of the History of Logic","Sets and Extensions in the Twentieth Century"],"original-title":[],"deposited":{"date-parts":[[2019,6,27]],"date-time":"2019-06-27T17:09:25Z","timestamp":1561655365000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444516213500098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"references-count":60,"URL":"https:\/\/doi.org\/10.1016\/b978-0-444-51621-3.50009-8","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2012]]}}}