Show simple item record

dc.contributor.authorParmann, Erik
dc.date.accessioned2016-03-22T10:07:04Z
dc.date.available2016-03-22T10:07:04Z
dc.date.issued2015
dc.identifier.urihttps://hdl.handle.net/1956/11725
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.language.isoengeng
dc.publisherDagstuhl Publishingen_US
dc.relation.ispartof<a href="http://hdl.handle.net/1956/11718" target="blank">Case Studies in Constructive Mathematics</a>en_US
dc.rightsAttribution CC BY 3.0eng
dc.rights.urihttp://creativecommons.org/licenses/by/3.0eng
dc.subjectType theoryeng
dc.subjectConstructive Logiceng
dc.subjectFinite Setseng
dc.titleInvestigating Streamless Setsen_US
dc.typeConference object
dc.typePeer reviewed
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright Erik Parmannen_US
dc.identifier.doihttps://doi.org/10.4230/lipics.types.2014.187
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400en_US


Files in this item

Thumbnail

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