Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation
Functional Kan simplicial sets are simplicial sets in which the horn-fillers required by the Kan extension condition are given explicitly by functions. We show the non-constructivity of the following basic result: if B and A are functional Kan simplicial sets, then A^B is a Kan simplicial set. This strengthens a similar result for the case of non-functional Kan simplicial sets shown by Bezem, Coquand and Parmann [TLCA 2015, v. 38 of LIPIcs]. Our
result shows that-from a constructive point of view-functional
Kan simplicial sets are, as it stands, unsatisfactory as a model of even simply typed lambda calculus. Our proof is based on a rather involved Kripke countermodel which has been encoded and verified in the Coq proof assistant.
constructive logic
simplicial sets
semantics of simple types
8:1-8:25
Regular Paper
Erik
Parmann
Erik Parmann
10.4230/LIPIcs.TYPES.2015.8
M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In R. Matthes and A. Schubert, editors, Proc. of 19th Int. Conf. on Types for Proofs and Programs, TYPES 2013, volume 26 of Leibniz Int. Proc. in Inf., pages 107-128. Dagstuhl Publishing, 2014. URL: http://dx.doi.org/10.4230/lipics.types.2013.107.
http://dx.doi.org/10.4230/lipics.types.2013.107
M. Bezem, T. Coquand, and E. Parmann. Non-constructivity in Kan simplicial sets. In T. Altenkirch, editor, Proc. of 13th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2015, volume 38 of Leibniz Int. Proc. in Inf., pages 92-106. Dagstuhl Publishing, 2015. URL: http://dx.doi.org/10.4230/lipics.tlca.2015.92.
http://dx.doi.org/10.4230/lipics.tlca.2015.92
Marc Bezem and Thierry Coquand. A Kripke model for simplicial sets. Theor. Comput. Sci., 574:86-91, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.01.035.
http://dx.doi.org/10.1016/j.tcs.2015.01.035
The Coq Development Team. The Coq reference manual, version 8.4, 2012. URL: https://coq.inria.fr/distrib/8.4/refman/.
https://coq.inria.fr/distrib/8.4/refman/
R. Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51(1):176-178, 1975. URL: http://dx.doi.org/10.1090/s0002-9939-1975-0373893-x.
http://dx.doi.org/10.1090/s0002-9939-1975-0373893-x
G. Friedman. An elementary illustrated introduction to simplicial sets. arXiv preprint 0809.4221, 2008. URL: https://arxiv.org/abs/0809.4221.
https://arxiv.org/abs/0809.4221
P. Goerss and J. F. Jardine. Simplicial Homotopy Theory, volume 174 of Progress in Mathematics. BirkhĂ¤user, 1999. Reprinted in Modern BirkhĂ¤user Classics, 2009. URL: http://dx.doi.org/10.1007/978-3-0348-8707-6.
http://dx.doi.org/10.1007/978-3-0348-8707-6
C. Kapulkin, P. LeFanu Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. arXiv preprint 1211.2851, 2012. URL: https://arxiv.org/abs/1211.2851.
https://arxiv.org/abs/1211.2851
S. Kripke. Semantical analysis of intuitionistic logic I. In M. Dummett and J.N. Crossley, editors, Formal Systems and Recursive Functions, volume 40 of Studies in Logic and the Foundations of Mathematics, pages 92-130. North Holland, 1965. URL: http://dx.doi.org/10.1016/s0049-237x(08)71685-9.
http://dx.doi.org/10.1016/s0049-237x(08)71685-9
J. P. May. Simplicial Objects in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 2nd edition, 1993.
J. C. Moore. Algebraic homotopy theory. Lectures at Princeton, 1956. URL: http://faculty.tcu.edu/gfriedman/notes/aht1.pdf.
http://faculty.tcu.edu/gfriedman/notes/aht1.pdf
T. Nikolaus. Algebraic models for higher categories. Indag. Math., 21(1-2):52-75, 2011. URL: http://dx.doi.org/10.1016/j.indag.2010.12.004.
http://dx.doi.org/10.1016/j.indag.2010.12.004
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode