×

Unifying exact completions. (English) Zbl 1386.03074

Summary: We define the notion of exact completion with respect to an existential elementary doctrine. We observe that the forgetful functor from the 2-category of exact categories to existential elementary doctrines has a left biadjoint that can be obtained as a composite of two others. Finally, we conclude how this notion encompasses both that of the exact completion of a regular category as well as that of the exact completion of a category with binary products, a weak terminal object and weak pullbacks.

MSC:

03G30 Categorical logic, topoi
03B15 Higher-order logic; type theory (MSC2010)
18C50 Categorical semantics of formal languages
03F55 Intuitionistic mathematics
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] 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-120. Springer-Verlag (1971) · Zbl 0223.18009
[2] Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261-293 (2003) · Zbl 1060.03030 · doi:10.1017/S0956796802004501
[3] Carboni, A.: Analysis non-standard e topos. Rend. Istit. Mat. Univ. Trieste 14(1-2), 1-16 (1982) · Zbl 0536.03050
[4] Carboni, A.: Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103, 117-148 (1995) · Zbl 0839.18002 · doi:10.1016/0022-4049(94)00103-P
[5] Carboni, A., Celia Magno, R.: The free exact category on a left exact one. J. Aust. Math. Soc. 33(A), 295-301 (1982) · Zbl 0504.18005 · doi:10.1017/S1446788700018735
[6] 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-42. Springer-Verlag, New Orleans (1988) · Zbl 0651.18004
[7] Carboni, A., Vitale, E.: Regular and exact completions. J. Pure Appl. Algebra 125, 79-117 (1998) · Zbl 0891.18002 · doi:10.1016/S0022-4049(96)00115-6
[8] Carboni, A., Walters, R.: Cartesian bicategories. J. Pure Appl. Algebra 49, 11-32 (1987) · Zbl 0637.18003 · doi:10.1016/0022-4049(87)90121-6
[9] Coquand, T.: Metamathematical investigation of a calculus of constructions. In: Odifreddi, P. (ed.) Logic in Computer Science, pp. 91-122. Academic Press (1990) · Zbl 0504.18005
[10] Frey, J.: A 2-categorical analysis of the tripos-to-topos construction. arXiv:1104.2776v1 [math.CT] (2011) · Zbl 0637.18003
[11] Freyd, P., Scedrov, A.: Categories Allegories. North Holland Publishing Company (1991) · Zbl 0698.18002
[12] Hughes, J., Jacobs, B.: Factorization systems and fibrations: toward a fibred Birkhoff variety theorem. Electron. Notes Theor. Comput. Sci. 11 (2002) · Zbl 1270.18003
[13] Hyland, J.M.E., Johnstone, P.T., Pitts, A.M.: Tripos theory. Math. Proc. Camb. Phil. Soc. 88, 205-232 (1980) · Zbl 0451.03027 · doi:10.1017/S0305004100057534
[14] Jacobs, B.: Categorical Logic and Type Theory. North Holland Publishing Company (1999) · Zbl 0911.03001
[15] Kelly, G.: A note on relations relative to a factorization system. In: Carboni, A., Pedicchio, M., Rosolini, G. (eds.) Category Theory ’90. Lecture Notes in Mathematical, vol. 1488, pp. 249-261. Springer-Verlag, Como (1992) · Zbl 0736.18001
[16] Lawvere, F.W.: Adjointness in foundations. Dialectica 23, 281-296 (1969) · Zbl 0341.18002 · doi:10.1111/j.1746-8361.1969.tb01194.x
[17] 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-145. Springer (1969)
[18] 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-14. American Mathematical Society (1970) · Zbl 0234.18002
[19] Lawvere, F.W., Rosebrugh, R.: Sets for Mathematics. Cambridge University Press (2003) · Zbl 1031.18001
[20] Maietti, M.: A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160(3), 319-354 (2009) · Zbl 1186.03075 · doi:10.1016/j.apal.2009.01.006
[21] Maietti,M., Rosolini, G.: Elementary quotient completion. Theory Appl. Categ. 27(17), 445-463 (2013) · Zbl 1288.03048
[22] Maietti, M., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Log. Univers. 7(3), 371-402 (2013) · Zbl 1288.03049 · doi:10.1007/s11787-013-0080-2
[23] Maietti, M.E.: Joyal’s arithmetic universe as list-arithmetic pretopos. Theory Appl. Categ. 3(24), 39-83 (2010) · Zbl 1245.03111
[24] Nordström, B., Petersson, K., Smith, J.: Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford (1990) · Zbl 0744.03029
[25] Pasquali, F.: A co-free construction for elementary doctrines. To appear in Applied Categorical Structures (2013) · Zbl 1305.03064
[26] Pitts, A.M.: Tripos theory in retrospect. Math. Struct. Comput. Sci. 12(3), 265-279 (2002) · Zbl 1005.18005
[27] Succi Cruciani, R.: La teoria delle relazioni nello studio di categorie regolari e di categorie esatte. Riv. Mat. Univ. Parma (4) 1, 143-158 (1975) · Zbl 0356.18004
[28] van Oosten, J.: Realizability: An Introduction to its Categorical Side, vol. 152. North Holland Publishing Company (2008) · Zbl 1225.03002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.