{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T05:00:14Z","timestamp":1777525214501,"version":"3.51.4"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T00:00:00Z","timestamp":1386201600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Appl Categor Struct"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10485-013-9360-5","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T13:40:19Z","timestamp":1386164419000},"page":"43-52","source":"Crossref","is-referenced-by-count":28,"title":["Unifying Exact Completions"],"prefix":"10.1007","volume":"23","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Rosolini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,12,5]]},"reference":[{"key":"9360_CR1","doi-asserted-by":"crossref","unstructured":"Barr, M.: Exact categories. In: Barr, M., Grillet, P., van Osdol, D. (eds.) Exact Categories and Categories of Sheaves. Lecture Notes in Mathematical, vol. 236, pp. 1\u2013120. Springer-Verlag (1971)","DOI":"10.1007\/BFb0058580"},{"issue":"2","key":"9360_CR2","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"issue":"1\u20132","key":"9360_CR3","first-page":"1","volume":"14","author":"A Carboni","year":"1982","unstructured":"Carboni, A.: Analysis non-standard e topos. Rend. Istit. Mat. Univ. Trieste 14(1\u20132), 1\u201316 (1982)","journal-title":"Rend. Istit. Mat. Univ. Trieste"},{"key":"9360_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. Algebra 103, 117\u2013148 (1995)","journal-title":"J. Pure Appl. Algebra"},{"issue":"A","key":"9360_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. Aust. Math. Soc. 33(A), 295\u2013301 (1982)","journal-title":"J. Aust. Math. Soc."},{"key":"9360_CR6","doi-asserted-by":"crossref","unstructured":"Carboni, A., Freyd, P., Scedrov, A.: A categorical approach to realizability and polymorphic types. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Mathematical Foundations of Programming Language Semantics. Lectures Notes in Computer Science, vol. 298, pp. 23\u201342. Springer-Verlag, New Orleans (1988)","DOI":"10.1007\/3-540-19020-1_2"},{"key":"9360_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.: Regular and exact completions. J. Pure Appl. Algebra 125, 79\u2013117 (1998)","journal-title":"J. Pure Appl. Algebra"},{"key":"9360_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-4049(87)90121-6","volume":"49","author":"A Carboni","year":"1987","unstructured":"Carboni, A., Walters, R.: Cartesian bicategories. J. Pure Appl. Algebra 49, 11\u201332 (1987)","journal-title":"J. Pure Appl. Algebra"},{"key":"9360_CR9","unstructured":"Coquand, T.: Metamathematical investigation of a calculus of constructions. In: Odifreddi, P. (ed.) Logic in Computer Science, pp. 91\u2013122. Academic Press (1990)"},{"key":"9360_CR10","unstructured":"Frey, J.: A 2-categorical analysis of the tripos-to-topos construction. arXiv: 1104.2776v1 [math.CT] (2011)"},{"key":"9360_CR11","unstructured":"Freyd, P., Scedrov, A.: Categories Allegories. North Holland Publishing Company (1991)"},{"key":"9360_CR12","unstructured":"Hughes, J., Jacobs, B.: Factorization systems and fibrations: toward a fibred Birkhoff variety theorem. Electron. Notes Theor. Comput. Sci. 11 (2002)"},{"key":"9360_CR13","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","volume":"88","author":"JME Hyland","year":"1980","unstructured":"Hyland, J.M.E., Johnstone, P.T., Pitts, A.M.: Tripos theory. Math. Proc. Camb. Phil. Soc. 88, 205\u2013232 (1980)","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"9360_CR14","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. North Holland Publishing Company (1999)"},{"key":"9360_CR15","doi-asserted-by":"crossref","unstructured":"Kelly, G.: A note on relations relative to a factorization system. In: Carboni, A., Pedicchio, M., Rosolini, G. (eds.) Category Theory \u201990. Lecture Notes in Mathematical, vol. 1488, pp. 249\u2013261. Springer-Verlag, Como (1992)","DOI":"10.1007\/BFb0084224"},{"key":"9360_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","volume":"23","author":"FW Lawvere","year":"1969","unstructured":"Lawvere, F.W.: Adjointness in foundations. Dialectica 23, 281\u2013296 (1969)","journal-title":"Dialectica"},{"key":"9360_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. Two), pp. 134\u2013145. Springer (1969)"},{"key":"9360_CR18","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Proceedings New York Symposium on Application of Categorical Algebra, pp. 1\u201314. American Mathematical Society (1970)","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"9360_CR19","doi-asserted-by":"crossref","unstructured":"Lawvere, F.W., Rosebrugh, R.: Sets for Mathematics. Cambridge University Press (2003)","DOI":"10.1017\/CBO9780511755460"},{"issue":"3","key":"9360_CR20","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/j.apal.2009.01.006","volume":"160","author":"M Maietti","year":"2009","unstructured":"Maietti, M.: A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160(3), 319\u2013354 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"17","key":"9360_CR21","first-page":"445","volume":"27","author":"M Maietti","year":"2013","unstructured":"Maietti,M., Rosolini, G.: Elementary quotient completion. Theory Appl. Categ. 27(17), 445\u2013463 (2013)","journal-title":"Theory Appl. Categ."},{"issue":"3","key":"9360_CR22","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/s11787-013-0080-2","volume":"7","author":"M Maietti","year":"2013","unstructured":"Maietti, M., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Log. Univers. 7(3), 371\u2013402 (2013)","journal-title":"Log. Univers."},{"issue":"24","key":"9360_CR23","first-page":"39","volume":"3","author":"ME Maietti","year":"2010","unstructured":"Maietti, M.E.: Joyal\u2019s arithmetic universe as list-arithmetic pretopos. Theory Appl. Categ. 3(24), 39\u201383 (2010)","journal-title":"Theory Appl. Categ."},{"key":"9360_CR24","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin L\u00f6f\u2019s Type Theory. Clarendon Press, Oxford (1990)"},{"key":"9360_CR25","doi-asserted-by":"crossref","unstructured":"Pasquali, F.: A co-free construction for elementary doctrines. To appear in Applied Categorical Structures (2013)","DOI":"10.1007\/s10485-013-9358-z"},{"issue":"3","key":"9360_CR26","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1017\/S096012950200364X","volume":"12","author":"AM Pitts","year":"2002","unstructured":"Pitts, A.M.: Tripos theory in retrospect. Math. Struct. Comput. Sci. 12(3), 265\u2013279 (2002)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9360_CR27","first-page":"143","volume":"1","author":"R Succi Cruciani","year":"1975","unstructured":"Succi Cruciani, R.: La teoria delle relazioni nello studio di categorie regolari e di categorie esatte. Riv. Mat. Univ. Parma (4) 1, 143\u2013158 (1975)","journal-title":"Riv. Mat. Univ. Parma (4)"},{"key":"9360_CR28","unstructured":"van Oosten, J.: Realizability: An Introduction to its Categorical Side, vol. 152. North Holland Publishing Company (2008)"}],"container-title":["Applied Categorical Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10485-013-9360-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10485-013-9360-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10485-013-9360-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,4]],"date-time":"2019-08-04T08:13:27Z","timestamp":1564906407000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10485-013-9360-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,5]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["9360"],"URL":"https:\/\/doi.org\/10.1007\/s10485-013-9360-5","relation":{},"ISSN":["0927-2852","1572-9095"],"issn-type":[{"value":"0927-2852","type":"print"},{"value":"1572-9095","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,5]]}}}