{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:21:08Z","timestamp":1784233268365,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665373","type":"print"},{"value":"9783540481676","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48167-2_12","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T07:40:19Z","timestamp":1191570019000},"page":"166-178","source":"Crossref","is-referenced-by-count":8,"title":["About Effective Quotients in Constructive Type Theory"],"prefix":"10.1007","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. The type theoretic interpretation of constructive set theory. In L. Paris MacIntyre, A. Pacholski, editor, Logic Colloquium\u2019 77. North Holland, Amsterdam, 1978. 166","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"12_CR2","volume-title":"Toposes and Local Set Theories: an introduction","author":"J.L. Bell","year":"1988","unstructured":"J.L. Bell. Toposes and Local Set Theories: an introduction. Claredon Press, Oxford, 1988. 171"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"1265","DOI":"10.2307\/2275642","volume":"62","author":"J.L. Bell","year":"1997","unstructured":"J.L. Bell. Zorn\u2019s lemma and complete boolean algebras in intuitionistic type theories. The Journal of Symbolic Logic., 62:1265\u20131279, 1997. 166","journal-title":"The Journal of Symbolic Logic"},{"key":"12_CR4","unstructured":"R. Constable et al. Implementing mathematics with the Nuprl Development System. Prentice Hall, 1986. 166, 175"},{"key":"12_CR5","unstructured":"T. Coquand. Pattern matching with dependent types. In Workshop on logical frameworks, Baastad, 1992. Preliminary Proceedings. 164, 170"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"176","DOI":"10.2307\/2039868","volume":"51","author":"R. Diaconescu","year":"1975","unstructured":"R. Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51:176\u2013178, 1975. 165, 166, 171","journal-title":"Proc. Amer. Math. Soc."},{"key":"12_CR7","unstructured":"P. Dybier. A general formulation of simultaneous inductive-recursive definitions in type theory. 1997. To appear in Journal of Symbolic Logic. 170"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1002\/malq.19780242514","volume":"24","author":"N. Goodman","year":"1978","unstructured":"N. Goodman and J. Myhill. Choice implies excluded middle. Z. Math. Logik Grundlag. Math., 24:461, 1978. 166","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"12_CR9","unstructured":"M. Hofmann. Extensional concept in intensional type theory. PhD thesis, University of Edinburgh, July 1995. 164, 167, 169, 170, 171"},{"key":"12_CR10","first-page":"83","volume-title":"Twenty Five Years of Constructive Type Theory","author":"M. Hofmann","year":"1995","unstructured":"M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In J. Smith G. Sambin, editor, Twenty Five Years of Constructive Type Theory, pages 83\u2013111. Oxford Science Publications, Venice, 1995. 164, 170"},{"key":"12_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Types\u2019 96","author":"M.E. Maietti","year":"1997","unstructured":"M.E. Maietti. The internal type theory of an Heyting Pretopos. In E. Gimenez and C. Paulin-Mohring, editors, Proceedings of Types\u2019 96, LNCS, 1997. 166, 177"},{"key":"12_CR12","unstructured":"M.E. Maietti. The type theory of categorical universes. PhD thesis, University of Padova, February 1998. 177"},{"key":"12_CR13","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples, 1984. 164, 168, 170, 171"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"M. Makkai and G. Reyes. First order categorical logic., volume 611 of Lecture Notes in Mathematics. Springer Verlag, 1977. 164","DOI":"10.1007\/BFb0066201"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"M.E. Maietti and S. Valentini. Can you add power-sets to Martin-L\u00f6f intuitionistic type theory? 1999. To appear in Mathematical Logic Quarterly. 171, 172","DOI":"10.1002\/malq.19990450410"},{"key":"12_CR16","volume-title":"Programming in Martin L\u00f6f\u2019 s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Peterson, and J. Smith. Programming in Martin L\u00f6f\u2019 s Type Theory. Clarendon Press, Oxford, 1990. 164, 167, 168, 169, 170, 172, 173, 176"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.2307\/2275645","volume":"62","author":"S. Negri","year":"1997","unstructured":"S. Negri and S. Valentini. Tychonoff\u2019s theorem in the framework of formal topologies. Journal of Symbolic Logic, 62:1315\u20131332, 1997. 164","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"G. Sambin. Intuitionistic formal spaces-a first communication. Mathematical logic and its applications, pages 187\u2013204, 1987. 164","DOI":"10.1007\/978-1-4613-0897-3_12"},{"key":"12_CR19","first-page":"275","volume-title":"Twenty Five Years of Constructive Type Theory","author":"S. Valentini","year":"1995","unstructured":"S. Valentini. The forget-restore principle: a paradigmatic example. In J. Smith G. Sambin, editor, Twenty Five Years of Constructive Type Theory, pages 275\u2013283. Oxford Science Publications, Venice, 1995. 164, 168"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48167-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T15:06:17Z","timestamp":1556895977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48167-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665373","9783540481676"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-48167-2_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}