2026-07-24T05:46:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11407 2024-03-06T10:46:04Z ddc:004 open_access

Dependent Sums and Dependent Products in Bishop’s Set Theory Petrakis, Iosif Bishop’s constructive mathematics Martin-Löf’s type theory dependent sums dependent products type-theoretic axiom of choice 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Iosif Petrakis 2019 Is Part Of LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2018.3 urn:nbn:de:0030-drops-114070 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.3 eng https://creativecommons.org/licenses/by/3.0/legalcode