Exact completion and constructive theories of sets. (English) Zbl 1485.03257
Setoids in Martin-Löf type theory arise as the exact completion of the category of closed types. Such categories, called quasi-Cartesian categories by the authors, have finite products but only weak equalizers. More generally, any model of the constructive elementary theory of the category of sets (CETCS) is the exact completion of its projective objects, which satisfy a categorical version of the axiom of choice and form a quasi-Cartesian category.
In this paper, the authors isolate two properties of a quasi-Cartesian category \(\mathcal C\) that are satisfied by the category of closed types in Martin-Löf type theory and that ensure that its exact completion is a model of CETCS. They give a categorical formulation of Aczel’s fullness axiom from constructive Zermelo-Fraenkel set theory in \(\mathcal C\) that ensures local Cartesian closure of its exact completion. They also give a complete characterization of well-pointed exact completions in terms of their projectives.
In this paper, the authors isolate two properties of a quasi-Cartesian category \(\mathcal C\) that are satisfied by the category of closed types in Martin-Löf type theory and that ensure that its exact completion is a model of CETCS. They give a categorical formulation of Aczel’s fullness axiom from constructive Zermelo-Fraenkel set theory in \(\mathcal C\) that ensures local Cartesian closure of its exact completion. They also give a complete characterization of well-pointed exact completions in terms of their projectives.
Reviewer: Amit Kuber (Kanpur)
MSC:
| 03G30 | Categorical logic, topoi |
| 18A35 | Categories admitting limits (complete categories), functors preserving limits, completions |
| 18B25 | Topoi |
| 18A15 | Foundations, relations to logic and deductive systems |
| 03B38 | Type theory |
| 18B05 | Categories of sets, characterizations |
| 18D15 | Closed categories (closed monoidal and Cartesian closed categories, etc.) |
| 03F55 | Intuitionistic mathematics |
Keywords:
setoids; exact completion; local Cartesian closure; constructive set theory; categorical logicSoftware:
GitHubReferences:
| [1] | Aczel, P., The type theoretic interpretation of constructive set theory, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics (Macintyre, A., Pacholski, L., and Paris, J., editors), North-Holland, Amsterdam, 1978, pp. 55-66. · Zbl 0481.03035 |
| [2] | Aczel, P. and Rathjen, M., Notes on constructive set theory. Technical report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, Stockholm, 2001. |
| [3] | Van Den Berg, B., Inductive types and exact completion. Annals of Pure and Applied Logic, vol. 134 (2005), no. 2, pp. 95-121. · Zbl 1064.03041 |
| [4] | Van Den Berg, B. and Moerdijk, I., Aspects of predicative algebraic set theory I: Exact completion. Annals of Pure and Applied Logic, vol. 156 (2008), no. 1, pp. 123-159. · Zbl 1165.03045 |
| [5] | Van Den Berg, B. and Moerdijk, I., Exact completion of path categories and algebraic set theory. Part I: Exact completion of path categories. Journal of Pure and Applied Algebra, vol. 222 (2018), no. 10, pp. 3137-3181. · Zbl 1420.18034 |
| [6] | Birkedal, L., Carboni, A., Rosolini, G., and Scott, D. S., Type theory via exact categories (extended abstract), Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science LICS ’98, IEEE Computer Society Press, New York, 1998, pp. 188-198. · Zbl 0945.03542 |
| [7] | Bishop, E., Foundations of constructive analysis , McGraw-Hill Series in Higher Mathematics, McGraw-Hill, New York, 1967. · Zbl 0183.01503 |
| [8] | Carboni, A., Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra, vol. 103 (1995), no. 2, pp. 117-148. · Zbl 0839.18002 |
| [9] | Carboni, A. and Magno, R. C., The free exact category on a left exact one. Journal of the Australian Mathematical Society, vol. 33 (1982), no. 3, pp. 295-301. · Zbl 0504.18005 |
| [10] | Carboni, A. and Rosolini, G., Locally cartesian closed exact completions. Journal of Pure and Applied Algebra, vol. 154 (2000), no. 1-3, pp. 103-116. · Zbl 0962.18001 |
| [11] | Carboni, A. and Vitale, E. M., Regular and exact completions. Journal of Pure and Applied Algebra, vol. 125 (1998), no. 1-3, pp. 79-116. · Zbl 0891.18002 |
| [12] | Coquand, T., Dybjer, P., Palmgren, E., and Setzer, A., Type-Theoretic Foundation of Constructive Mathematics. Notes distributed at the TYPES Summer School, Göteborg, Sweden, 2005. |
| [13] | Emmenegger, J., The Fullness Axiom and exact completions of homotopy categories . Cahiers de Topologie et Géométrie Différentielle Catégoriques, to appear. Preprint available from. arXiv:1808.09905 |
| [14] | Emmenegger, J., On the local cartesian closure of exact completions. Journal of Pure and Applied Algebra, vol. 224 (2020), no. 11, pp. 1-25. · Zbl 1436.18003 |
| [15] | Gandy, R., On the axiom of extensionality - Part I , this vol. 21 (1956), no. 1, pp. 36-48. · Zbl 0073.00801 |
| [16] | Gran, M. and Vitale, E. M., On the exact completion of the homotopy category. Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 39 (1998), no. 4, pp. 287-297. · Zbl 0918.18003 |
| [17] | Grandis, M., Weak subobjects and weak limits in categories and homotopy categories. Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 38 (1997), no. 4, pp. 301-326. · Zbl 0891.18001 |
| [18] | Grandis, M., Weak subobjects and the epi-monic completion of a category. Journal of Pure and Applied Algebra, vol. 154 (2000), no. 1, pp. 193-212. · Zbl 1059.18001 |
| [19] | Hofmann, M., On the interpretation of type theory in locally Cartesian closed categories. Computer Science Logic, Springer, Berlin, Heidelberg, 1995, pp. 427-441. · Zbl 1044.03544 |
| [20] | Lawvere, F. W., Adjointness in foundations. Dialectica, vol. 23 (1969), pp. 281-296. · Zbl 0341.18002 |
| [21] | Lawvere, F. W., Adjoints in and among bicategories, Logic and Algebra (Ursini, A., editor), Routledge, Abingdon, 1996. · Zbl 0862.18002 |
| [22] | Maietti, M. E. and Rosolini, G., Elementary quotient completion. Theory and Applications of Categories, vol. 27 (1969), no. 17, pp. 445-463. · Zbl 1288.03048 |
| [23] | Maietti, M. E. and Rosolini, G., Quotient completion for the foundation of constructive mathematics. Logica Universalis, vol. 7 (2013), no. 3, pp. 371-402. · Zbl 1288.03049 |
| [24] | Maietti, M. E. and Rosolini, G., Relating quotient completions via categorical logic, Concepts of Proof in Mathematics, Philosophy, and Computer Science (Schuster, P. and Probst, D., editors), De Gruyter, Berlin, 2016, pp. 229-250. · Zbl 1433.03164 |
| [25] | Martin-Löf, P., 100 years of Zermelo’s Axiom of choice: What was the problem with it?. The Computer Journal, vol. 49 (2006), no. 3, pp. 345-350. |
| [26] | Moerdijk, I. and Palmgren, E., Wellfounded trees in categories. Annals of Pure and Applied Logic, vol. 104 (2000), no. 1, pp. 189-218. · Zbl 1010.03056 |
| [27] | Nordström, B., Petersson, K., and Smith, J. M., Programming in Martin-Löf’s type theory. An introduction, Oxford University Press, Oxford, 1990. · Zbl 0744.03029 |
| [28] | Palmgren, E., A categorical version of the Brouwer-Heyting-Kolmogorov interpretation. Mathematical Structures in Computer Science, vol. 14 (2004), no. 1, pp. 57-72. · Zbl 1051.03054 |
| [29] | Palmgren, E., Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets. Annals of Pure and Applied Logic, vol. 163 (2012), no. 10, pp. 1384-1399. · Zbl 1257.03095 |
| [30] | Palmgren, E., LCC setoids in Coq. GitHub repository, 2012. Available at https://github.com/erikhpalmgren/LCC.setoids.in.Coq. |
| [31] | Palmgren, E., Categories with families, FOLDS and logic enriched type theory, 2016, arXiv:1605.01586. |
| [32] | Palmgren, E. and Wilander, O., Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science, vol. 10 (2014), no. 3. · Zbl 1341.03012 |
| [33] | Robinson, E. and Rosolini, G., Colimit completions and the effective topos , this , vol. 55 (1990), no. 2, pp. 678-699. · Zbl 0713.18003 |
| [34] | . Homotopy Type Theory: Univalent Foundations in Mathematics, Institute for Advanced Studies, Princeton, 2013. Available at http://homotopytypetheory.org/. · Zbl 1298.03002 |
| [35] | Wilander, O., Setoids and universes. Mathematical Structures in Computer Science, vol. 20 (2010), no. 4, pp. 563-576. · Zbl 1204.03060 |
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.
