License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TLCA.2015.92
URN: urn:nbn:de:0030-drops-51579
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5157/
Go to the corresponding LIPIcs Volume Portal

Bezem, Marc ; Coquand, Thierry ; Parmann, Erik

Non-Constructivity in Kan Simplicial Sets

pdf-format:
12.pdf (0.5 MB)

Abstract

We 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.

BibTeX - Entry

@InProceedings{bezem_et_al:LIPIcs:2015:5157,
  author =	{Marc Bezem and Thierry Coquand and Erik Parmann},
  title =	{{Non-Constructivity in Kan Simplicial Sets}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{92--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Thorsten Altenkirch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5157},
  URN =		{urn:nbn:de:0030-drops-51579},
  doi =		{10.4230/LIPIcs.TLCA.2015.92},
  annote =	{Keywords: Constructive logic, simplicial sets, semantics of simple types}
}

Keywords: Constructive logic, simplicial sets, semantics of simple types
Collection: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Issue Date: 2015
Date of publication: 15.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI