Document Open Access Logo

Towards a Cubical Type Theory without an Interval

Authors Thorsten Altenkirch, Ambrus Kaposi

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2015.3.pdf
  • Filesize: 0.58 MB
  • 27 pages

Document Identifiers

Author Details

Thorsten Altenkirch
Ambrus Kaposi

Cite AsGet BibTex

Thorsten Altenkirch and Ambrus Kaposi. Towards a Cubical Type Theory without an Interval. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2015.3

Abstract

Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g., a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we do not know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
Keywords
  • homotopy type theory
  • parametricity
  • univalence

Metrics

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

References

  1. Thorsten Altenkirch and James Chapman. Big-step normalisation. J. Funct. Program., 19(3-4):311-333, 2009. URL: http://dx.doi.org/10.1017/S0956796809007278.
  2. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837638.
  3. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Aaron Stump and Hongwei Xi, editors, Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007, pages 57-68. ACM, 2007. URL: http://dx.doi.org/10.1145/1292597.1292608.
  4. C. Angiuli, R. Harper, and T. Wilson. Computational higher-dimensional type theory. In Proc. of 44th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2017, pages 680-693. ACM, 2017. URL: http://dx.doi.org/10.1145/3009837.3009861.
  5. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 503-516. ACM, 2014. URL: http://dx.doi.org/10.1145/2535838.2535852.
  6. J.-P. Bernardy and G. Moulin. A computational interpretation of parametricity. In Proc. of 27th Ann. IEEE Symp. on Logic in Computer Science, LICS '12, pages 135-144. IEEE, 2012. URL: http://dx.doi.org/10.1109/lics.2012.25.
  7. 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.
  8. 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.
  9. 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.
  10. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Comput. Surv., 17(4):471-522, 1985. URL: http://dx.doi.org/10.1145/6041.6042.
  11. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. In T. Uustalu, editor, Proc. of 21st Int. Conf. on Types for Proofs and Programs, TYPES 2015, volume 69 of Leibniz Int. Proc. in Inform. Dagstuhl Publishing, 2017. Google Scholar
  12. T. Coquand. Variation on cubical sets. Note, 2014. URL: http://www.cse.chalmers.se/~coquand/comp.pdf.
  13. Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. Logical relations and parametricity - A Reynolds programme for category theory and programming languages. Electr. Notes Theor. Comput. Sci., 303:149-180, 2014. URL: http://dx.doi.org/10.1016/j.entcs.2014.02.008.
  14. S. Huber. A Model of Type Theory in Cubical Sets. Licentiate thesis, Chalmers University of Technology, 2015. URL: http://www.cse.chalmers.se/~simonhu/misc/lic.pdf.
  15. G. Moulin. Pure Type Systems with an Internalized Parametricity Theorem. Licentiate thesis, Chalmers University of Technology, 2013. URL: http://publications.lib.chalmers.se/publication/191873.
  16. G. Moulin. Internalizing Parametricity. PhD thesis, Chalmers University of Technology, 2016. URL: http://publications.lib.chalmers.se/publication/235758.
  17. A. Polonsky. Extensionality of lambda-*. 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.
  18. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/.
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