eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-12
187
201
10.4230/LIPIcs.TYPES.2014.187
article
Investigating Streamless Sets
Parmann, Erik
In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless.
We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol039-types2014/LIPIcs.TYPES.2014.187/LIPIcs.TYPES.2014.187.pdf
Type theory
Constructive Logic
Finite Sets