LIPIcs.TYPES.2015.8.pdf
- Filesize: 0.52 MB
- 25 pages
Document
Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation
Author
-
Part of:
Volume:
21st International Conference on Types for Proofs and Programs (TYPES 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-03-15
Cite As Get BibTex
Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 8:1-8:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.8
Abstract
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.
Subject Classification
Keywords
- constructive logic
- simplicial sets
- semantics of simple types
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- 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.
- 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.
- The Coq Development Team. The Coq reference manual, version 8.4, 2012. URL: 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.
- G. Friedman. An elementary illustrated introduction to simplicial sets. arXiv preprint 0809.4221, 2008. URL: 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.
- 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.
- 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.
-
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.
- 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.