Show simple item record

dc.contributor.authorParmann, Erik
dc.description.abstractIn 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.en_US
dc.publisherDagstuhl Publishingen_US
dc.relation.ispartof<a href="" target="blank">Case Studies in Constructive Mathematics</a>en_US
dc.rightsAttribution CC BY 3.0eng
dc.subjectType theoryeng
dc.subjectConstructive Logiceng
dc.subjectFinite Setseng
dc.titleInvestigating Streamless Setsen_US
dc.typeConference object
dc.typePeer reviewed
dc.rights.holderCopyright Erik Parmannen_US
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400en_US

Files in this item


This item appears in the following Collection(s)

Show simple item record

Attribution CC BY 3.0
Except where otherwise noted, this item's license is described as Attribution CC BY 3.0