Document Open Access Logo

Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation

Author Erik Parmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2015.8.pdf
  • Filesize: 0.52 MB
  • 25 pages

Document Identifiers

Subject Classification

Keywords
  • constructive logic
  • simplicial sets
  • semantics of simple types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Erik Parmann

References

  1. 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.
  2. 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.
  3. 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.
  4. The Coq Development Team. The Coq reference manual, version 8.4, 2012. URL: https://coq.inria.fr/distrib/8.4/refman/.
  5. 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.
  6. G. Friedman. An elementary illustrated introduction to simplicial sets. arXiv preprint 0809.4221, 2008. URL: https://arxiv.org/abs/0809.4221.
  7. 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.
  8. 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.
  9. 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.
  10. J. P. May. Simplicial Objects in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 2nd edition, 1993. Google Scholar
  11. J. C. Moore. Algebraic homotopy theory. Lectures at Princeton, 1956. URL: http://faculty.tcu.edu/gfriedman/notes/aht1.pdf.
  12. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact