Document Open Access Logo

Non-Constructivity in Kan Simplicial Sets

Authors Marc Bezem, Thierry Coquand, Erik Parmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.92.pdf
  • Filesize: 0.48 MB
  • 15 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

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.

Cite As Get BibTex

Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.92

Author Details

Marc Bezem
Thierry Coquand
Erik Parmann

References

  1. Steve Awodey and Michael Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45-55, 2009. Google Scholar
  2. Marc Bezem and Thierry Coquand. A Kripke model for simplicial sets. TCS, 2015. doi:10.1016/j.tcs.2015.01.035. Google Scholar
  3. Greg Friedman. An elementary illustrated introduction to simplicial sets. Preprint, http://arxiv.org/abs/0809.4221, 2008.
  4. Peter Gabriel and Michel Zisman. Calculus of fractions and homotopy theory. Springer, 1967. Google Scholar
  5. Paul Goerss and J.F. Jardine. Simplicial Homotopy Theory. Modern Birkhäuser Classics. Birkhauser Verlag GmbH, 2009. Reprint of Vol. 174 of Progress in Mathematics, 1999. Google Scholar
  6. Martin Hofmann. Syntax and semantics of dependent types. In A.M. Pitts and P. Dybjer, editors, Semantics and logics of computation, volume 14 of Publ. Newton Inst., pages 79-130. Cambridge University Press, Cambridge, 1997. Google Scholar
  7. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations. Preprint, http://arxiv.org/abs/1211.2851, 2012.
  8. Saul Kripke. Semantical analysis of intuitionistic logic I. In M. Dummett and J.N. Crossley, editors, Formal Systems and Recursive Functions, pages 92-130. North-Holland, Amsterdam, 1965. Google Scholar
  9. Bob Lubarsky, March 2015. Personal communication. Google Scholar
  10. Jon Peter May. Simplicial Objects in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 2nd edition, 1993. Google Scholar
  11. Charles McCarty. Two questions about IZF and intuitionistic validity. Pdf file, personal communication, March 2015. Google Scholar
  12. John C. Moore. Algebraic homotopy theory. Lectures at Princeton, http://faculty.tcu.edu/gfriedman/notes/aht1.pdf, 1956.
  13. Thomas Nikolaus. Algebraic models for higher categories. Preprint, http://arxiv.org/abs/1003.1342, 2010.
  14. Vladimir Voevodsky. Notes on type systems. http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf, 2009.
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