Document

# Dependent Sums and Dependent Products in Bishop’s Set Theory

## File

LIPIcs.TYPES.2018.3.pdf
• Filesize: 0.58 MB
• 21 pages

## Acknowledgements

I want to thank the Hausdorff Research Institute for Mathematics (HIM) for providing me with ideal conditions of work as a temporary project fellow of the trimester program "Types, Sets and Constructions" (July-August 2018). It was during this stay of mine in Bonn that most of the research around this paper was carried out.

## Cite As

Iosif Petrakis. Dependent Sums and Dependent Products in Bishop’s Set Theory. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.3

## Abstract

According to the standard, non type-theoretic accounts of Bishop’s constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman’s sense, semi-formalisation of Bishop’s set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Constructive mathematics
##### Keywords
• Bishop’s constructive mathematics
• Martin-Löf’s type theory
• dependent sums
• dependent products
• type-theoretic axiom of choice

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Peter Aczel and Michael Rathjen. Notes on Constructive Set Theory. Technical report, Institut Mittag-Leffler Preprint, 2000.
2. Steven Awodey. Axiom of Choice and Excluded Middle in Categorical Logic. Bulletin of Symbolic Logic, 1:344, 1995.
3. Michael J. Beeson. Formalizing constructive mathematics: Why and how? In Constructive Mathematics, pages 146-190. Springer Berlin Heidelberg, 1981. URL: https://doi.org/10.1007/bfb0090733.
4. Michael J. Beeson. Foundations of Constructive Mathematics. Springer Berlin Heidelberg, 1985. URL: https://doi.org/10.1007/978-3-642-68952-9.
5. Errett Bishop. Foundations of Constructive Analysis. Mcgraw-Hill, 1967.
6. Errett Bishop. A General Lamguage. unpublished manuscript, 1968(9)?
7. Errett Bishop. How to Compile Mathematics into Algol. unpublished manuscript, 1968(9)?
8. Errett Bishop. Mathematics as a Numerical Language. In Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, pages 53-71. Elsevier, 1970. URL: https://doi.org/10.1016/s0049-237x(08)70740-7.
9. Errett Bishop and Douglas S. Bridges. Constructive Analysis. Grundlehren der mathematischen Wissenschaften. Springer Berlin Heidelberg, 1985.
10. Douglas S. Bridges and Fred Richman. Varieties of constructive mathematics. Cambridge University Press, 1987.
11. Thierry Coquand, Peter Dybjer, Erik Palmgren, and Anton Setzer. Type-theoretic Foundations of Constructive Mathematics. book draft, 2005.
12. Thierry Coquand and Henrik Persson. Integrated Development of Algebra in Type Theory. manuscript, 1998.
13. Thierry Coquand and Arnaud Spiwack. Towards Constructive Homological Algebra in Type Theory. In Towards Mechanized Mathematical Assistants, pages 40-54. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73086-6_4.
14. James Dugundji. Topology. Allyn and Bacon series in advanced mathematics. Allyn and Bacon, 1966.
15. Robert Lee Constable et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
16. Solomon Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, pages 87-139. Springer Berlin Heidelberg, 1975. URL: https://doi.org/10.1007/bfb0062852.
17. Solomon Feferman. Constructive Theories of Functions and Classes. In Studies in Logic and the Foundations of Mathematics, pages 159-224. Elsevier, 1979. URL: https://doi.org/10.1016/s0049-237x(08)71625-2.
18. Harvey Friedman. Set Theoretic Foundations for Constructive Analysis. The Annals of Mathematics, 105(1):1, January 1977. URL: https://doi.org/10.2307/1971023.
19. Newcomb Greenleaf. Liberal constructive set theory. In Constructive Mathematics, pages 213-240. Springer Berlin Heidelberg, 1981.
20. Hajime Ishihara and Erik Palmgren. Quotient topologies in constructive set theory and type theory. Annals of Pure and Applied Logic, 141(1-2):257-265, August 2006. URL: https://doi.org/10.1016/j.apal.2005.11.005.
21. Maria Emilia Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, September 2009. URL: https://doi.org/10.1016/j.apal.2009.01.006.
22. Per Martin-Löf. Notes on Constructive Mathematics. Almqvist and Wiksell, 1968.
23. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium quotesingle73, Proceedings of the Logic Colloquium, pages 73-118. Elsevier, 1975. URL: https://doi.org/10.1016/s0049-237x(08)71945-1.
24. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
25. Ray Mines, Fred Richman, and Wim Ruitenburg. A course in constructive algebra. Springer-Verlag, 1988.
26. John Myhill. Constructive set theory. Journal of Symbolic Logic, 40(3):347-382, September 1975. URL: https://doi.org/10.2307/2272159.
27. Erik Palmgren. Bishop’s set theory. Slides from TYPES Summer School 2005, Gothenburg, 2005.
28. Erik Palmgren. Lecture Notes on Type Theory. manuscript, 2014.
29. Erik Palmgren and Olov Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science, Volume 10, Issue 3, 2014. URL: https://doi.org/10.2168/LMCS-10(3:25)2014.
30. Iosif Petrakis. Constructive topology of Bishop spaces. PhD thesis, Ludwig-Maximilians-University, Munich, 2015.
31. Iosif Petrakis. A constructive function-theoretic approach to topological compactness. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS quotesingle16. ACM Press, 2016. URL: https://doi.org/10.1145/2933575.2933582.
32. Iosif Petrakis. The Urysohn Extension Theorem for Bishop Spaces. In Logical Foundations of Computer Science, pages 299-316. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-27683-0_21.
33. Iosif Petrakis. Constructive uniformities of pseudometrics and Bishop topologies. Journal of Logic and Analysis, 11:FT2:1-44, 2019.
34. Iosif Petrakis. Direct spectra of Bishop spaces and their limits. arXiv:1907.03273, 2019.
35. Iosif Petrakis. Constructive Set and Function Theory. habilitation, Ludwig-Maximilians-University, Munich, in preparation, 2020.
36. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, 2013.
37. Giovanni Sambin. The Basic Picture: Structures for Constructive Topology. Oxford University Press, in press, 2019.
38. Tilo Wiklund. Locally cartesian closed categories, coalgebras, and containers. Technical report, Uppsala Universitet, U.U.D.M Project Report, 2013.
X

Feedback for Dagstuhl Publishing