License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2018.3
URN: urn:nbn:de:0030-drops-114070
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11407/
Go to the corresponding LIPIcs Volume Portal

Petrakis, Iosif

Dependent Sums and Dependent Products in Bishop's Set Theory

pdf-format:
LIPIcs-TYPES-2018-3.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{petrakis:LIPIcs:2019:11407,
  author =	{Iosif Petrakis},
  title =	{{Dependent Sums and Dependent Products in Bishop's Set Theory}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Peter Dybjer and Jos{\'e} Esp{\'\i}rito Santo and Lu{\'\i}s Pinto},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11407},
  URN =		{urn:nbn:de:0030-drops-114070},
  doi =		{10.4230/LIPIcs.TYPES.2018.3},
  annote =	{Keywords: Bishop's constructive mathematics, Martin-L{\"o}f's type theory, dependent sums, dependent products, type-theoretic axiom of choice}
}

Keywords: Bishop's constructive mathematics, Martin-Löf's type theory, dependent sums, dependent products, type-theoretic axiom of choice
Collection: 24th International Conference on Types for Proofs and Programs (TYPES 2018)
Issue Date: 2019
Date of publication: 18.11.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI