{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T02:27:45Z","timestamp":1783132065890,"version":"3.54.6"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,5,5]],"date-time":"2013-05-05T00:00:00Z","timestamp":1367712000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1007\/s11787-013-0080-2","type":"journal-article","created":{"date-parts":[[2013,5,4]],"date-time":"2013-05-04T07:23:47Z","timestamp":1367652227000},"page":"371-402","source":"Crossref","is-referenced-by-count":40,"title":["Quotient Completion for the Foundation of Constructive Mathematics"],"prefix":"10.1007","volume":"7","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giuseppe","family":"Rosolini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,5,5]]},"reference":[{"issue":"2","key":"80_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G. Barthes","year":"2003","unstructured":"Barthes G., Capretta V., Pons O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"80_CR2","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Carboni, A., Rosolini, G., Scott, D.S.: Type theory via exact categories. In: Pratt, V. (ed.) Proc. 13th Symposium in Logic in Computer Science, pp. 188\u2013198, IEEE Computer Society, Indianapolis (1998)","DOI":"10.1109\/LICS.1998.705655"},{"key":"80_CR3","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop E.: Foundations of Constructive Analysis. McGraw-Hill, Maidenheach (1967)"},{"key":"80_CR4","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0022-4049(94)00103-P","volume":"103","author":"A. Carboni","year":"1995","unstructured":"Carboni A.: Some free constructions in realizability and proof theory. J. Pure Appl. Alg. 103, 117\u2013148 (1995)","journal-title":"J. Pure Appl. Alg."},{"issue":"A","key":"80_CR5","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1017\/S1446788700018735","volume":"33","author":"A. Carboni","year":"1982","unstructured":"Carboni A., Celia Magno R.: The free exact category on a left exact one. J. Austr. Math. Soc. 33(A), 295\u2013301 (1982)","journal-title":"J. Austr. Math. Soc."},{"key":"80_CR6","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0022-4049(99)00192-9","volume":"154","author":"A. Carboni","year":"2000","unstructured":"Carboni A., Rosolini G.: Locally cartesian closed exact completions. J. Pure Appl. Alg. 154, 103\u2013116 (2000)","journal-title":"J. Pure Appl. Alg."},{"key":"80_CR7","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0022-4049(96)00115-6","volume":"125","author":"A. Carboni","year":"1998","unstructured":"Carboni A., Vitale E.M.: Regular and exact completions. J. Pure Appl. Alg. 125, 79\u2013117 (1998)","journal-title":"J. Pure Appl. Alg."},{"key":"80_CR8","unstructured":"Coquand, T.: Metamathematical investigation of a calculus of constructions. In: Odifreddi, P. (ed.) Logic in Computer Science, pp. 91\u2013122. Academic Press, Dublin (1990)"},{"key":"80_CR9","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Internal type theory. In: TYPES \u201995. Lecture Notes in Computer Science, vol. 1158, pp. 120\u2013134. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61780-9_66"},{"key":"80_CR10","volume-title":"Categories Allegories","author":"P.J. Freyd","year":"1991","unstructured":"Freyd P.J., Scedrov A.: Categories Allegories. North Holland Publishing Co, Amsterdam (1991)"},{"key":"80_CR11","doi-asserted-by":"crossref","unstructured":"Grothendieck, A.: Cat\u00e9gories fibr\u00e9es et descent (Expos\u00e9 VI). In: Grothendieck, A. (ed.) Rev\u00eatements etales et groupe fondamental\u2014SGA 1. Lecture Notes in Mathematics, vol. 224, pp. 145\u2013194. Springer, Berlin (1971)","DOI":"10.1007\/BFb0058662"},{"key":"80_CR12","doi-asserted-by":"crossref","unstructured":"Hofmann M. Extensional Constructs in Intensional Type Theory. Distinguished Dissertations. Springer, Berlin (1997)","DOI":"10.1007\/978-1-4471-0963-1"},{"key":"80_CR13","unstructured":"Hughes, J., Jacobs, B.: Factorization systems and fibrations: toward a fibred Birkhoff variety theorem. Electron. Notes Theor. Comp. Sci. 11 (2002)"},{"key":"80_CR14","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs B.: Categorical Logic and Type Theory. North-Holland Publishing Co, Amsterdam (1999)"},{"key":"80_CR15","volume-title":"Introduction to higher order categorical logic","author":"J. Lambek","year":"1986","unstructured":"Lambek J., Scott P.J.: Introduction to higher order categorical logic. Cambridge University Press, Cambridge (1986)"},{"key":"80_CR16","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Adjointness in foundations. Dialectica 23, 281\u2013296 (1969)","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"80_CR17","unstructured":"Lawvere, F.W.: Diagonal arguments and cartesian closed categories. In: Category Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, vol. 2), pp. 134\u2013145. Springer, Berlin (1969)"},{"key":"80_CR18","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Proc. New York Symposium on Application of Categorical Algebra, pp. 1\u201314. Amer. Math. Soc., New York (1970)","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"80_CR19","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511755460","volume-title":"Sets for Mathematics","author":"F.W. Lawvere","year":"2003","unstructured":"Lawvere F.W., Rosebrugh R.: Sets for Mathematics. Cambridge University Press, Cambridge (2003)"},{"issue":"6","key":"80_CR20","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1017\/S0960129505004962","volume":"15","author":"M.E. Maietti","year":"2005","unstructured":"Maietti M.E.: Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Structures Comp. Sci., 15(6), 1089\u20131149 (2005)","journal-title":"Math. Structures Comp. Sci.,"},{"issue":"3","key":"80_CR21","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/j.apal.2009.01.006","volume":"160","author":"M.E. Maietti","year":"2009","unstructured":"Maietti M.E.: A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160(3), 319\u2013354 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"key":"80_CR22","unstructured":"Maietti, M.E.: Consistency of the minimalist foundation with Church thesis and Bar Induction (2010, submitted)"},{"key":"80_CR23","doi-asserted-by":"crossref","unstructured":"Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: Crosilla L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics. Oxford Logic Guides, vol. 48, pp. 91\u2013114. Oxford University Press, New York (2005)","DOI":"10.1093\/acprof:oso\/9780198566519.003.0006"},{"key":"80_CR24","doi-asserted-by":"crossref","unstructured":"Makkai M., Reyes G. First Order Categorical Logic. Lecture Notes in Mathematics, vol. 611. Springer, Berlin (1977)","DOI":"10.1007\/BFb0066201"},{"key":"80_CR25","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin -L\u00f6f\u2019s Type Theory. Clarendon Press, Oxford (1990)"},{"key":"80_CR26","unstructured":"Palmgren, E.: Bishop\u2019s set theory. Slides for a lecture at the TYPES summer school (2005)"},{"issue":"2","key":"80_CR27","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1093\/jigpal\/4.2.159","volume":"4","author":"D. Pavlovi\u0107","year":"1996","unstructured":"Pavlovi\u0107 D.: Maps II: chasing proofs in the Lambek\u2013Lawvere logic. Log. J. IGPL. 4(2), 159\u2013194 (1996)","journal-title":"Log. J. IGPL."},{"key":"80_CR28","doi-asserted-by":"crossref","unstructured":"Sambin G., Valentini, S.: Building up a toolbox for Martin\u2013L\u00f6f\u2019s type theory: subset theory. In: Sambin, G., Smith, J. (eds.) Twenty-five years of constructive type theory, pp. 221\u2013244. Oxford University Press, Oxford (1998)","DOI":"10.1093\/oso\/9780198501275.003.0014"},{"key":"80_CR29","doi-asserted-by":"crossref","unstructured":"Streicherm, Th.: Semantics of type theory. Birkh\u00e4user, Boston (1991)","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"80_CR30","volume-title":"Practical Foundations of Mathematics","author":"P. Taylor","year":"1999","unstructured":"Taylor P.: Practical Foundations of Mathematics. Cambridge University Press, Cambridge (1999)"},{"key":"80_CR31","unstructured":"van Oosten, J. Realizability: An Introduction to its Categorical Side, vol. 152. North-Holland Publishing Co., Amsterdam (2008)"}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-013-0080-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-013-0080-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-013-0080-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:35:28Z","timestamp":1746002128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-013-0080-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,5]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,9]]}},"alternative-id":["80"],"URL":"https:\/\/doi.org\/10.1007\/s11787-013-0080-2","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,5]]}}}