Document Open Access Logo

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Authors Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2015.5.pdf
  • Filesize: 0.65 MB
  • 34 pages

Document Identifiers

Author Details

Cyril Cohen
Thierry Coquand
Simon Huber
Anders Mörtberg

Cite AsGet BibTex

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.5

Abstract

This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
Keywords
  • univalence axiom
  • dependent type theory
  • cubical sets

Metrics

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

References

  1. Peter Aczel. On relating type theories and set theories. In Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus, editors, Types for Proofs and Programs, International Workshop TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers, volume 1657 of Lecture Notes in Computer Science, pages 1-18. Springer, 1998. URL: http://dx.doi.org/10.1007/3-540-48167-2_1.
  2. T. Altenkirch. Extensional equality in intensional type theory. In Proc. of 14th Ann. IEEE Symp. on Logic in Computer Science, LICS '99, pages 412-420. IEEE, 1999. URL: http://dx.doi.org/10.1109/lics.1999.782636.
  3. R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1974. Reprinted by Abstract Space Publishing in 2011. Google Scholar
  4. Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. Electr. Notes Theor. Comput. Sci., 319:67-82, 2015. URL: http://dx.doi.org/10.1016/j.entcs.2015.12.006.
  5. Jean-Philippe Bernardy and Guilhem Moulin. Type-theory in color. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 61-72. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500577.
  6. 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 Inform., pages 107-128. Dagstuhl Publishing, 2014. URL: http://dx.doi.org/10.4230/lipics.types.2013.107.
  7. R. Brown, P. J. Higgins, and R. Sivera. Nonabelian Algebraic Topology: Filtered Spaces, Crossed Complexes, Cubical Homotopy Groupoids, volume 15 of EMS Tracts in Mathematics. Europ. Math. Soc., 2011. URL: http://dx.doi.org/10.4171/083.
  8. D.-C. Cisinski. Univalent universes for elegant models of homotopy types, 2014. arXiv preprint 1406.0058. URL: https://arxiv.org/abs/1406.0058.
  9. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_66.
  10. M. Fourman and D. Scott. Sheaves and logic. In M. Fourman, C. Mulvey, and D. Scott, editors, Applications of Sheaves, volume 753 of Lect. Notes in Math., pages 302-401. Springer, 1979. URL: http://dx.doi.org/10.1007/bfb0061824.
  11. N. Gambino and C. Sattler. Uniform fibrations and the Frobenius condition, 2015. arXiv preprint 1510.00669. URL: https://arxiv.org/abs/1510.00669.
  12. M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, volume 14 of Publications of the Newton Institute, pages 79-130. Cambridge University Press, 1997. URL: http://dx.doi.org/10.1017/cbo9780511526619.004.
  13. S. Huber. A Model of Type Theory in Cubical Sets. Licentiate thesis, University of Gothenburg, 2015. URL: http://www.cse.chalmers.se/~simonhu/misc/lic.pdf.
  14. S. Huber. Canonicity for cubical type theory, 2016. arXiv preprint 1607.04156. URL: https://arxiv.org/abs/1607.04156.
  15. J. A. Kalman. Lattices with involution. Trans. Amer. Math. Soc., 87:485-491, 1958. URL: http://dx.doi.org/10.1090/s0002-9947-1958-0095135-x.
  16. D. M. Kan. Abstract homotopy I. Proc. Nat. Acad. Sci. USA, 41(12):1092-1096, 1955. URL: http://www.pnas.org/content/41/12/1092.full.pdf.
  17. C. Kapulkin and P. LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), 2012. arXiv preprint 1211.2851. URL: https://arxiv.org/abs/1211.2851.
  18. D. R. Licata and G. Brunerie. A cubical approach to synthetic homotopy theory. In Proc. of 30th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS '15, pages 92-103. IEEE, 2015. URL: http://dx.doi.org/10.1109/lics.2015.19.
  19. P. Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North Holland, 1975. URL: http://dx.doi.org/10.1016/s0049-237x(08)71945-1.
  20. P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. M. Smith, editors, Twenty-Five Years of Constructive Type Theory, volume 36 of Oxford Logic Guides, pages 127-172. Clarendon Press, 1998. Google Scholar
  21. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. URL: http://dx.doi.org/10.1017/cbo9781139084673.
  22. A. M. Pitts. Nominal presentation of cubical sets models of type theory. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, Proc. of 20th Int. Conf. on Types for Proofs and Programs, TYPES 2014, volume 39 of Leibniz Int. Proc. in Inform., pages 202-220. Dagstuhl Publishing, 2015. URL: http://dx.doi.org/10.4230/lipics.types.2014.202.
  23. A. Polonsky. Extensionality of λ∗. In H. Herbelin, P. Letouzey, and M. Sozeau, editors, Proc. of 20th Int. Conf. on Types for Proofs and Programs, TYPES 2014, volume 39 of Leibniz Int. Proc. in Inform., pages 221-250. Dagstuhl Publishing, 2015. URL: http://dx.doi.org/10.4230/lipics.types.2014.221.
  24. T. Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Progress in Theoretical Computer Science. Birkhäuser, 1991. URL: http://dx.doi.org/10.1007/978-1-4612-0433-6.
  25. A. Swan. An algebraic weak factorisation system on 01-substitution sets: A constructive proof, 2014. arXiv preprint 1409.1829. URL: https://arxiv.org/abs/1409.1829.
  26. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  27. V. Voevodsky. The equivalence axiom and univalent models of type theory (talk at CMU on feb. 4, 2010), 2014. arXiv preprint 1402.5556. URL: https://arxiv.org/abs/1402.5556.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact