{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T15:23:56Z","timestamp":1648740236154},"reference-count":28,"publisher":"Elsevier BV","issue":"10","license":[{"start":{"date-parts":[[2012,10,1]],"date-time":"2012-10-01T00:00:00Z","timestamp":1349049600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,10,1]],"date-time":"2016-10-01T00:00:00Z","timestamp":1475280000000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1016\/j.apal.2012.01.013","type":"journal-article","created":{"date-parts":[[2012,2,16]],"date-time":"2012-02-16T07:48:43Z","timestamp":1329378523000},"page":"1419-1436","source":"Crossref","is-referenced-by-count":0,"title":["Constructive toposes with countable sums as models of constructive set theory"],"prefix":"10.1016","volume":"163","author":[{"given":"Alex","family":"Simpson","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Streicher","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.apal.2012.01.013_br000005","series-title":"Logic Colloquium \u201977","first-page":"55","article-title":"The type theoretic interpretation of constructive set theory","volume":"vol. 96","author":"Aczel","year":"1978"},{"key":"10.1016\/j.apal.2012.01.013_br000010","series-title":"Logic, Methodology and Philosophy of Science VII","article-title":"The type theoretic interpretation of constructive set theory: Inductive definitions","author":"Aczel","year":"1986"},{"key":"10.1016\/j.apal.2012.01.013_br000015","unstructured":"P. Aczel, M. Rathjen, Notes on constructive set theory, Technical Report 40, 2000\/2001, Mittag-Leffler Institute, Sweden, 2001."},{"key":"10.1016\/j.apal.2012.01.013_br000020","unstructured":"S. Awodey, C. Butz, A.K. Simpson, Th. Streicher, Relating first-order set theories, toposes and categories of classes, Ann.\u00a0Pure Appl.\u00a0Logic (under revision)."},{"issue":"5","key":"10.1016\/j.apal.2012.01.013_br000025","first-page":"147","article-title":"Algebraic models of intuitionistic theories of sets and classes","volume":"15","author":"Awodey","year":"2005","journal-title":"Theory Appl. Categ."},{"issue":"1","key":"10.1016\/j.apal.2012.01.013_br000030","first-page":"1","article-title":"Predicative algebraic set theory","volume":"15","author":"Awodey","year":"2005","journal-title":"Theory Appl. Categ."},{"key":"10.1016\/j.apal.2012.01.013_br000035","unstructured":"B. van den Berg, Predicative Topos Theory and Models for Constructive Set Theory, Ph.D. Thesis, Utrecht University, 2006."},{"issue":"1","key":"10.1016\/j.apal.2012.01.013_br000040","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/j.apal.2008.06.013","article-title":"Aspects of predicative algebraic set theory I: exact completion","volume":"156","author":"van den Berg","year":"2008","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/j.apal.2012.01.013_br000045","series-title":"Logic Colloquium 2006","first-page":"18","article-title":"A unified approach to algebraic set theory","author":"van den Berg","year":"2009"},{"key":"10.1016\/j.apal.2012.01.013_br000050","unstructured":"B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory III: sheaves, 2010. Preprint: http:\/\/arxiv.org\/abs\/0912.1242."},{"key":"10.1016\/j.apal.2012.01.013_br000055","doi-asserted-by":"crossref","unstructured":"B. van den Berg, I. Moerdijk, Aspects of predicative algebraic set theory II: realizability, Theoretical Computer Science (in press).","DOI":"10.1016\/j.tcs.2010.12.019"},{"key":"10.1016\/j.apal.2012.01.013_br000060","doi-asserted-by":"crossref","unstructured":"L. Birkedal, A. Carboni, G. Rosolini, D.S. Scott, Type theory via exact categories, in: Proc.\u00a0Logic in Computer Science (LICS), 1998, pp. 188\u2013198.","DOI":"10.1109\/LICS.1998.705655"},{"key":"10.1016\/j.apal.2012.01.013_br000065","series-title":"Handbook of Categorical Algebra, vol. 3","author":"Borceux","year":"1994"},{"key":"10.1016\/j.apal.2012.01.013_br000070","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0022-4049(80)90096-1","article-title":"Sheaf models for set theory","volume":"19","author":"Fourman","year":"1980","journal-title":"J. Pure Appl. Algebra"},{"key":"10.1016\/j.apal.2012.01.013_br000075","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/1971023","article-title":"Set theoretic foundations for constructive analysis","volume":"105","author":"Friedman","year":"1977","journal-title":"Ann. of Math."},{"key":"10.1016\/j.apal.2012.01.013_br000080","series-title":"Proceedings of the Logic Conference, Hakone","article-title":"On set theories and toposes","volume":"vol. 891","author":"Hayashi","year":"1980"},{"key":"10.1016\/j.apal.2012.01.013_br000085","series-title":"Sketches of an Elephant: a Topos Theory Compendium, Vols. 1\u20132","volume":"vol. 43\u201344","author":"Johnstone","year":"2002"},{"key":"10.1016\/j.apal.2012.01.013_br000090","series-title":"Algebraic Set Theory","volume":"vol. 220","author":"Joyal","year":"1995"},{"key":"10.1016\/j.apal.2012.01.013_br000095","series-title":"Sets for Mathematicians","author":"Lawvere","year":"2003"},{"key":"10.1016\/j.apal.2012.01.013_br000100","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1017\/S0960129502003663","article-title":"Impredicativity entails untypedness","volume":"12","author":"Lietz","year":"2002","journal-title":"Math. Structures Comput. Sci."},{"key":"10.1016\/j.apal.2012.01.013_br000105","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.apal.2004.08.002","article-title":"Independence results around constructive ZF","volume":"132","author":"Lubarsky","year":"2005","journal-title":"Ann.~Pure Appl.~Logic"},{"key":"10.1016\/j.apal.2012.01.013_br000110","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/S0022-4049(02)00261-X","article-title":"Characterization of the left exact categories whose exact completions are toposes","volume":"177","author":"Menni","year":"2003","journal-title":"J.~Pure Appl.~Algebra"},{"key":"10.1016\/j.apal.2012.01.013_br000115","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/S0168-0072(00)00012-9","article-title":"Well-founded trees in categories","volume":"104","author":"Moerdijk","year":"2000","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.apal.2012.01.013_br000120","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0168-0072(01)00079-3","article-title":"Type theories, toposes and constructive set theory: predicative aspects of AST","volume":"114","author":"Moerdijk","year":"2002","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.apal.2012.01.013_br000125","doi-asserted-by":"crossref","first-page":"347","DOI":"10.2307\/2272159","article-title":"Constructive set theory","volume":"40","author":"Myhill","year":"1975","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.apal.2012.01.013_br000130","series-title":"Realizability: an Introduction to its Categorical Side","volume":"vol. 152","author":"van Oosten","year":"2008"},{"key":"10.1016\/j.apal.2012.01.013_br000135","unstructured":"M.A. Shulman, Stack semantics and the comparison of material and structural set theories, 2010. Preprint: http:\/\/arxiv.org\/pdf\/1004.3802v1."},{"key":"10.1016\/j.apal.2012.01.013_br000140","doi-asserted-by":"crossref","unstructured":"A.K. Simpson, Elementary axioms for categories of classes, in: Proc. 14th Annual IEEE Symposium on Logic in Computer Science, 1999, pp. 77\u201385.","DOI":"10.1109\/LICS.1999.782592"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007212000322?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007212000322?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,25]],"date-time":"2018-11-25T23:23:01Z","timestamp":1543188181000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007212000322"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10]]},"references-count":28,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["S0168007212000322"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2012.01.013","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2012,10]]}}}