Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets. (English) Zbl 1257.03095

Comparing Bishop’s informal set theory with Lawvere’s elementary theory of the category of sets (ETCS), the author proposes a constructive and predicative version of ETCS whose standard model is based on the constructive type theory of Martin-Löf. The theory, CETCS, provides a structuralist foundation for constructive mathematics in the style of Bishop.
As one may expect, CETCS is classically equivalent to ETCS plus the Axiom of Choice and the Principle of Excluded Middle. Also, the theory allows to “reason using elements” which greatly simplifies its potential application, avoiding most of the rather complex categorical notions.
Nevertheless, a purely categorical characterisation of categorical models for CETCS is possible and the author shows it. This characterisation requires to show that the category is locally Cartesian closed, among a few other properties. Since deciding whether a category is locally Cartesian closed apparently requires the use of the Axiom of Choice in the meta-theory, the author reduces this check to the simpler task of verifying the validity of a specific axiom of CETCS. This last result has an independent value from CETCS and may be useful in other contexts.


03G30 Categorical logic, topoi
03B15 Higher-order logic; type theory (MSC2010)
18B05 Categories of sets, characterizations
18B25 Topoi
Full Text: DOI arXiv


[1] Aczel, P., The type theoretic interpretation of constructive set theory, (), 55-66
[2] Awodey, S.; Warren, M.A., Predicative algebraic set theory, Theory and applications of categories, 15, 1, 1-39, (2005/06) · Zbl 1072.18004
[3] Bishop, E., Foundations of constructive analysis, (1967), McGraw-Hill · Zbl 0183.01503
[4] Bishop, E., Mathematics as a numerical language, (), 53-71 · Zbl 0205.01201
[5] E. Bishop, Compiling Mathematics into Algol, Unpublished text for a seminar, 1970.
[6] Hofmann, M., On the interpretation of type theory in locally Cartesian closed categories, () · Zbl 1044.03544
[7] Johnstone, P.T., Sketches of an elephant: A topos theory compendium, vol. 1-2, (2002), Oxford University Press · Zbl 1071.18002
[8] Joyal, A.; Moerdijk, I., Algebraic set theory, (1995), Cambridge University Press · Zbl 0847.03025
[9] Lawvere, F.W., An elementary theory of the category of sets (long version), Theory and applications of categories, 11, 7-35, (2005) · Zbl 1072.18005
[10] Lawvere, F.W.; Rosebrugh, R., Sets for mathematics, (2003), Cambridge University Press · Zbl 1031.18001
[11] Mac Lane, S., Categories for the working Mathematician, (1998), Springer · Zbl 0906.18001
[12] Maietti, M.E., Modular correspondence between dependent type theories and categories including pretopoi and topoi, Mathematical structures in computer science, 15, 6, 1089-1149, (2005) · Zbl 1093.03042
[13] Maietti, M.E.; Sambin, G., Toward a minimalist foundation for constructive mathematics, (), 91-114 · Zbl 1115.03090
[14] Martin-Löf, P., An intuitionistic theory of types: predicative part, () · Zbl 0334.02016
[15] McLarty, C., Exploring categorical structuralism, Philosophia Mathematica, 12, 37-53, (2004) · Zbl 1051.18004
[16] McLarty, C., ETCS and philosophy of mathematics, Theory and applications of categories, 11, 2-4, (2005)
[17] Makkai, M., Avoiding the axiom of choice in general category theory, Journal of pure and applied algebra, 108, 109-173, (1996) · Zbl 0859.18001
[18] Moerdijk, I.; Palmgren, E., Well-founded trees in categories, Annals of pure and applied logic, 104, 189-218, (2000) · Zbl 1010.03056
[19] Moerdijk, I.; Palmgren, E., Type theories, toposes and constructive set theory: predicative aspects of AST, Annals of pure and applied logic, 114, 155-201, (2002) · Zbl 0999.03061
[20] Myhill, J., Constructive set theory, Journal of symbolic logic, 40, 3, 347-382, (1975) · Zbl 0314.02045
[21] Osius, G., Categorical set theory: a characterization of the category of sets, Journal of pure and applied algebra, 4, 79-119, (1974) · Zbl 0282.02027
[22] Palmgren, E., Locally Cartesian closed categories without chosen constructions, Theory and applications of category theory, 20, 5-17, (2008) · Zbl 1163.18003
[23] M.A. Shulman, Stack semantics and the comparison of material and structural set theories, April 2010. ArXiv:1004.3802v1.
[24] Tait, W.W., Cantor’s grundlagen and the paradoxes of set theory, (), 269-290, Also reprinted in W.W. Tait, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History, Oxford University Press, 2005 · Zbl 0984.03004
[25] van den Berg, B., Inductive types and exact completions, Annals of pure and applied logic, 134, 95-121, (2005) · Zbl 1064.03041
[26] van den Berg, B.; Moerdijk, I., Aspects of predicative algebraic set theory I: exact completion, Annals of pure and applied logic, 156, 123-159, (2008) · Zbl 1165.03045
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.