{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T23:17:13Z","timestamp":1693869433772},"reference-count":17,"publisher":"Elsevier BV","issue":"9","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2020,9,1]],"date-time":"2020-09-01T00:00:00Z","timestamp":1598918400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1016\/j.apal.2016.04.010","type":"journal-article","created":{"date-parts":[[2016,4,30]],"date-time":"2016-04-30T23:07:08Z","timestamp":1462057628000},"page":"794-805","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"title":["The intrinsic topology of Martin-L\u00f6f universes"],"prefix":"10.1016","volume":"167","author":[{"given":"Mart\u00edn H\u00f6tzel","family":"Escard\u00f3","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Streicher","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.apal.2016.04.010_br0010","series-title":"Computation, Meaning, and Logic: Articles Dedicated to Gordon Plotkin","first-page":"69","article-title":"A convenient category of domains","volume":"vol. 172","author":"Battenfeld","year":"2007"},{"issue":"2","key":"10.1016\/j.apal.2016.04.010_br0020","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.apal.2011.06.017","article-title":"Metric spaces in synthetic topology","volume":"163","author":"Bauer","year":"2012","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/j.apal.2016.04.010_br0030","series-title":"Foundations of Constructive Mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/j.apal.2016.04.010_br0040","article-title":"Varieties of Constructive Mathematics","volume":"vol. 97","author":"Bridges","year":"1987"},{"key":"10.1016\/j.apal.2016.04.010_br0050","author":"Escard\u00f3"},{"issue":"3","key":"10.1016\/j.apal.2016.04.010_br0070","doi-asserted-by":"crossref","first-page":"764","DOI":"10.2178\/jsl.7803040","article-title":"Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics","volume":"78","author":"Escard\u00f3","year":"2013","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.apal.2016.04.010_br0060","series-title":"Computability in Europe 2010, Abstract and Handout Booklet","first-page":"168","article-title":"Searchable sets, Dubuc\u2013Penon compactness, omniscience principles, and the Drinker Paradox","author":"Escard\u00f3","year":"2010"},{"key":"10.1016\/j.apal.2016.04.010_br0080","series-title":"Twenty-five Years of Constructive Type Theory","first-page":"83","article-title":"The groupoid interpretation of type theory","volume":"vol. 36","author":"Hofmann","year":"1998"},{"issue":"2","key":"10.1016\/j.apal.2016.04.010_br0090","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1112\/plms\/s3-38.2.237","article-title":"On a topological topos","volume":"38","author":"Johnstone","year":"1979","journal-title":"Proc. Lond. Math. Soc. (3)"},{"key":"10.1016\/j.apal.2016.04.010_br0100","series-title":"Stone Spaces","author":"Johnstone","year":"1982"},{"key":"10.1016\/j.apal.2016.04.010_br0110","series-title":"Sketches of an Elephant: a Topos Theory Compendium","author":"Johnstone","year":"2002"},{"issue":"5","key":"10.1016\/j.apal.2016.04.010_br0120","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129597002387","article-title":"A uniform approach to domain theory in realizability models","volume":"7","author":"Longley","year":"1997","journal-title":"Math. Structures Comput. Sci."},{"key":"10.1016\/j.apal.2016.04.010_br0130","series-title":"Twenty-five Years of Constructive Type Theory","first-page":"127","article-title":"An intuitionistic theory of types","volume":"vol. 36","author":"Martin-L\u00f6f","year":"1998"},{"key":"10.1016\/j.apal.2016.04.010_br0140","series-title":"Semantics of Type Theory","author":"Streicher","year":"1991"},{"key":"10.1016\/j.apal.2016.04.010_br0150","series-title":"From Sets and Types to Topology and Analysis","first-page":"78","article-title":"Universes in toposes","volume":"vol. 48","author":"Streicher","year":"2005"},{"key":"10.1016\/j.apal.2016.04.010_br0160","series-title":"Homotopy Type Theory, Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013"},{"key":"10.1016\/j.apal.2016.04.010_br0170","series-title":"Realizability. An Introduction to Its Categorical Side","author":"van Oosten","year":"2008"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007216300409?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007216300409?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,9,1]],"date-time":"2020-09-01T00:57:36Z","timestamp":1598921856000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007216300409"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":17,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["S0168007216300409"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2016.04.010","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2016,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The intrinsic topology of Martin-L\u00f6f universes","name":"articletitle","label":"Article Title"},{"value":"Annals of Pure and Applied Logic","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.apal.2016.04.010","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2016 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}