Document Open Access Logo

A Model of Type Theory in Cubical Sets

Authors Marc Bezem, Thierry Coquand, Simon Huber

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2013.107.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Subject Classification

Keywords
  • Models of dependent type theory
  • cubical sets
  • Univalent Foundations

Metrics

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

Abstract

We present a model of type theory with dependent product, sum, and
identity, in cubical sets. We describe a universe and explain how
to transform an equivalence between two types into an equality.  We
also explain how to model propositional truncation and the circle.
While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.

Cite As Get BibTex

Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 107-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.TYPES.2013.107

Author Details

Marc Bezem
Thierry Coquand
Simon Huber

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. Bruno Barras, Thierry Coquand, and Simon Huber. A generalization of Takeuti-Gandy interpretation. To appear in Mathematical Structures in Computer Science, 2013. Google Scholar
  3. Marc Bezem and Thierry Coquand. A Kripke model for simplicial sets. Preprint, 2013. Google Scholar
  4. Erret Bishop. Foundations of constructive analysis. McGraw-Hill Book Co., New York, 1967. Google Scholar
  5. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. Google Scholar
  6. Thierry Coquand and Nils Anders Danielsson. Isomorphism is equality. Indagationes Mathematicae, 24(4):1105-1120, 2013. Google Scholar
  7. Sjoerd Crans. On combinatorial models for higher dimensional homotopies. PhD thesis, Universiteit Utrecht, 1995. Google Scholar
  8. Pierre-Louis Curien. Substitutions up to isomorphisms. Fundamenta Informaticae, 19:51-85, 1993. Google Scholar
  9. Peter Dybjer. Internal type theory. In Types for Programs and Proofs, pages 120-134. Lecture Notes in Computer Science, Springer, 1996. Google Scholar
  10. Alexander Grothendieck. Pursuing stacks. Manuscript, 1983. Google Scholar
  11. 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
  12. Martin Hofmann and Thomas Streicher. Lifting Grothendieck universes. Unpublished Note. Google Scholar
  13. Simon Huber. A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2014. Google Scholar
  14. Witold Hurewicz. On the concept of fiber space. Proc. Nat. Acad. Sci. U. S. A., 41:956-961, 1955. Google Scholar
  15. Daniel M. Kan. Abstract homotopy. I. Proc. Nat. Acad. Sci. U. S. A., 41:1092-1096, 1955. Google Scholar
  16. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations. Preprint, http://arxiv.org/abs/1211.2851, 2012.
  17. Per Martin-Löf. An intiutionistic theory of types: Predicative part. In H. E. Rose and J. Shepherdson, editors, Logic Colloquium '73, pages 73-118. North-Holland, Amsterdam, 1975. Google Scholar
  18. Christine Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. In Marc Bezem and Jan Friso Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, 1993. Google Scholar
  19. Andrew M. Pitts. An equivalent presentation of the Bezem-Coquand-Huber category of cubical sets. Manuscript, http://arxiv.org/abs/1401.7807, September 2013.
  20. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  21. Jean-Pierre Serre. Homologie simgulière des espaces fibrés. Applications. Thèse, Paris, 1951. Google Scholar
  22. Allen Stoughton. Substitution revisited. Theoretical Computer Science, 59:317-325, 1988. Google Scholar
  23. Ross Street. Cosmoi of internal categories. Trans. Amer. Math. Soc., 258:271-318, 1980. Google Scholar
  24. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  25. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory. Talk at CMU, February 2010. Google Scholar
  26. Alfred N. Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, 2nd edition, 1925. Google Scholar
  27. Richard Williamson. Combinatorial homotopy theory. Preprint, 2012. Google Scholar
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