Investigating Streamless Sets
Journal article, Peer reviewed
Published version
Åpne
Permanent lenke
https://hdl.handle.net/1956/11725Utgivelsesdato
2015Metadata
Vis full innførselSamlinger
Originalversjon
https://doi.org/10.4230/lipics.types.2014.187Sammendrag
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.