2026-07-23T15:54:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5157 2024-03-06T10:36:10Z ddc:004 open_access

Non-Constructivity in Kan Simplicial Sets Bezem, Marc Coquand, Thierry Parmann, Erik Constructive logic simplicial sets semantics of simple types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marc Bezem and Thierry Coquand and Erik Parmann 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.92 urn:nbn:de:0030-drops-51579 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92 eng https://creativecommons.org/licenses/by/3.0/legalcode