Vis enkel innførsel

dc.contributor.authorBezem, Marc
dc.contributor.authorCoquand, Thierry
dc.contributor.authorParmann, Erik
dc.description.abstractWe give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.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.subjectconstructive logiceng
dc.subjectsimplicial setseng
dc.subjectsemantics of simple typeseng
dc.titleNon-Constructivity in Kan Simplicial Setsen_US
dc.typeConference object
dc.typePeer reviewed
dc.rights.holderCopyright Marc Bezem, Thierry Coquand, and Erik Parmannen_US
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400en_US

Tilhørende fil(er)


Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel

Attribution CC BY 3.0
Med mindre annet er angitt, så er denne innførselen lisensiert som Attribution CC BY 3.0