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: https://drops.dagstuhl.de/opus/volltexte/2015/5157/
Bezem, Marc ; Coquand, Thierry ; Parmann, Erik
Non-Constructivity in Kan Simplicial Sets
| pdf-format: |
|
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 | |
| Seminar: | 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 15.06.2015 |
