Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-24T16:41:52.476Z Has data issue: false hasContentIssue false
  • English
  • Français

EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS

Part of: Algebraic logic Proof theory and constructive mathematics Categories with structure Special categories General theory of categories and functors General logic

Published online by Cambridge University Press:  18 June 2020

JACOPO EMMENEGGER  and
ERIK PALMGREN
JACOPO EMMENEGGER
Affiliation:
DEPARTMENT OF MATHEMATICS STOCKHOLM UNIVERSITYSWEDENE-mail: [email protected] address: SCHOOL OF COMPUTER SCIENCE UNIVERSITY OF BIRMINGHAM, UK
ERIK PALMGREN
Affiliation:
DEPARTMENT OF MATHEMATICS STOCKHOLM UNIVERSITYSWEDEN
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e., objects satisfying the axiom of choice). Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS.

Keywords

setoidsexact completionlocal cartesian closureconstructive set theorycategorical logic

MSC classification

Primary: 03B15: Higher-order logic and type theory
Secondary: 18B05: Category of sets, characterizations 18D15: Closed categories (closed monoidal and Cartesian closed categories, etc.) 03F55: Intuitionistic mathematics 03G30: Categorical logic, topoi 18A35: Categories admitting limits (complete categories), functors preserving limits, completions
Type
Articles
Information
The Journal of Symbolic Logic , Volume 85 , Issue 2 , June 2020 , pp. 563 - 584
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Footnotes

*

Erik Palmgren passed away in 2019.

References

REFERENCES

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.Google Scholar
Aczel, P. and Rathjen, M., Notes on constructive set theory. Technical report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, Stockholm, 2001.Google Scholar
van den Berg, B., Inductive types and exact completion . Annals of Pure and Applied Logic, vol. 134 (2005), no. 2, pp. 95–121.10.1016/j.apal.2004.09.003CrossRefGoogle Scholar
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.10.1016/j.apal.2008.06.013CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Bishop, E., Foundations of constructive analysis , McGraw-Hill Series in Higher Mathematics, McGraw-Hill, New York, 1967.Google Scholar
Carboni, A., Some free constructions in realizability and proof theory . Journal of Pure and Applied Algebra, vol. 103 (1995), no. 2, pp. 117–148.CrossRefGoogle Scholar
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.10.1017/S1446788700018735CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.10.1016/S0022-4049(96)00115-6CrossRefGoogle Scholar
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.Google Scholar
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 Google Scholar
Emmenegger, J., On the local cartesian closure of exact completions . Journal of Pure and Applied Algebra, vol. 224 (2020), no. 11, pp. 1–25.10.1016/j.jpaa.2020.106414CrossRefGoogle Scholar
Gandy, R., On the axiom of extensionality – Part I , this vol. 21 (1956), no. 1, pp. 36–48.Google Scholar
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.Google Scholar
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.Google Scholar
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.10.1016/S0022-4049(99)00191-7CrossRefGoogle Scholar
Hofmann, M., On the interpretation of type theory in locally Cartesian closed categories . Computer Science Logic, Springer, Berlin, Heidelberg, 1995, pp. 427–441.10.1007/BFb0022273CrossRefGoogle Scholar
Lawvere, F. W., Adjointness in foundations . Dialectica, vol. 23 (1969), pp. 281–296.CrossRefGoogle Scholar
Lawvere, F. W., Adjoints in and among bicategories , Logic and Algebra (Ursini, A., editor), Routledge, Abingdon, 1996.Google Scholar
Maietti, M. E. and Rosolini, G., Elementary quotient completion . Theory and Applications of Categories, vol. 27 (1969), no. 17, pp. 445–463.Google Scholar
Maietti, M. E. and Rosolini, G., Quotient completion for the foundation of constructive mathematics . Logica Universalis, vol. 7 (2013), no. 3, pp. 371–402.10.1007/s11787-013-0080-2CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Moerdijk, I. and Palmgren, E., Wellfounded trees in categories . Annals of Pure and Applied Logic, vol. 104 (2000), no. 1, pp. 189–218.10.1016/S0168-0072(00)00012-9CrossRefGoogle Scholar
Nordström, B., Petersson, K., and Smith, J. M., Programming in Martin-Löf’s type theory. An introduction, Oxford University Press, Oxford, 1990.Google Scholar
Palmgren, E., A categorical version of the Brouwer-Heyting-Kolmogorov interpretation . Mathematical Structures in Computer Science, vol. 14 (2004), no. 1, pp. 57–72.10.1017/S0960129503003955CrossRefGoogle Scholar
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.10.1016/j.apal.2012.01.011CrossRefGoogle Scholar
Palmgren, E., LCC setoids in Coq. GitHub repository, 2012. Available at https://github.com/erikhpalmgren/LCC.setoids.in.Coq.Google Scholar
Palmgren, E., Categories with families, FOLDS and logic enriched type theory, 2016, arXiv:1605.01586.Google Scholar
Palmgren, E. and Wilander, O., Constructing categories and setoids of setoids in type theory . Logical Methods in Computer Science, vol. 10 (2014), no. 3.CrossRefGoogle Scholar
Robinson, E. and Rosolini, G., Colimit completions and the effective topos , this , vol. 55 (1990), no. 2, pp. 678–699.Google Scholar
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations in Mathematics, Institute for Advanced Studies, Princeton, 2013. Available at http://homotopytypetheory.org/.Google Scholar
Wilander, O., Setoids and universes . Mathematical Structures in Computer Science, vol. 20 (2010), no. 4, pp. 563–576.CrossRefGoogle Scholar