Document Open Access Logo

Cubical Syntax for Reflection-Free Extensional Equality

Authors Jonathan Sterling , Carlo Angiuli , Daniel Gratzer

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.31.pdf
  • Filesize: 0.74 MB
  • 25 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Algebraic semantics
  • Theory of computation → Denotational semantics
Keywords
  • Dependent type theory
  • extensional equality
  • cubical type theory
  • categorical gluing
  • canonicity

Metrics

Abstract

We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false.

Cite As Get BibTex

Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.31

Author Details

Jonathan Sterling
  • Carnegie Mellon University, Pittsburgh, USA
Carlo Angiuli
  • Carnegie Mellon University, Pittsburgh, USA
Daniel Gratzer
  • Aarhus University, Denmark

Funding

The authors gratefully acknowledge the support of the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.

Acknowledgements

We thank Lars Birkedal, Evan Cavallo, David Thrane Christiansen, Thierry Coquand, Kuen-Bang Hou (Favonia), Marcelo Fiore, Jonas Frey, Krzysztof Kapulkin, András Kovács, Dan Licata, Conor McBride, Darin Morrison, Anders Mörtberg, Michael Shulman, Bas Spitters, and Thomas Streicher for helpful conversations about extensional equality, algebraic type theory, and categorical gluing. We thank our anonymous reviewers for their insightful comments, and especially thank Robert Harper for valuable conversations throughout the development of this work. We also thank Paul Taylor for his diagrams package, which we have used to typeset the commutative diagrams in this paper.

References

  1. Andreas Abel, Thierry Coquand, and Peter Dybjer. On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. In Jacques Garrigue and Manuel V. Hermenegildo, editors, Functional and Logic Programming, pages 3-13. Springer Berlin Heidelberg, 2008. Google Scholar
  2. Stuart Frazier Allen. A non-type-theoretic semantics for type-theoretic language. phdthesis, Cornell University, 1987. Google Scholar
  3. Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 412-420, July 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782636.
  4. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:16. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.6.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type Theory in Type Theory Using Quotient Inductive Types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 18-29. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837638.
  6. Thorsten Altenkirch and Conor McBride. Towards Observational Type Theory, 2006. URL: https://www.strictlypositive.org/ott.pdf.
  7. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational Equality, Now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, PLPV '07, pages 57-68. ACM, 2007. Google Scholar
  8. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Syntax and Models of Cartesian Cubical Type Theory, February 2019. Preprint. URL: https://github.com/dlicata335/cart-cube.
  9. Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Anders Mörtberg, and Jonathan Sterling. color[rgb].91,.31,.27redtt: implementing Cartesian cubical type theory. Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory. URL: http://www.jonmsterling.com/pdfs/dagstuhl.pdf.
  10. Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, and Jonathan Sterling. The color[rgb].91,.31,.27RedPRL Proof Assistant (Invited Paper). In Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018., pages 1-10, 2018. URL: http://dx.doi.org/10.4204/EPTCS.274.1.
  11. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2018.6.
  12. Robert Atkey. Simplified Observational Type Theory, 2018. URL: https://github.com/bobatkey/sott.
  13. Steve Awodey. A cubical model of homotopy type theory. Annals of Pure and Applied Logic, 169(12):1270-1294, 2018. Logic Colloquium 2015. URL: http://dx.doi.org/10.1016/j.apal.2018.08.002.
  14. Steven Awodey and Andrej Bauer. Propositions As [Types]. J. Log. and Comput., 14(4):447-471, August 2004. URL: http://dx.doi.org/10.1093/logcom/14.4.447.
  15. Andrej Bauer, Gaëtan Gilbert, Philipp Haselwarter, Matija Pretnar, and Christopher A. Stone. Design and Implementation of the Andromeda proof assistant, 2016. TYPES. URL: http://www.types2016.uns.ac.rs/images/abstracts/bauer2.pdf.
  16. Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967. Google Scholar
  17. Andreas Blass. Words, free algebras, and coequalizers. Fundamenta Mathematicae, 117(2):117-160, 1983. URL: http://eudml.org/doc/211359.
  18. Edwin Brady, James Chapman, Pierre-Évariste Dagand, Adam Gundry, Conor McBride, Peter Morris, Ulf Norell, and Nicolas Oury. An Epigram Implementation, February 2011. Google Scholar
  19. John Cartmell. Generalised Algebraic Theories and Contextual Categories. phdthesis, Oxford University, January 1978. Google Scholar
  20. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. Google Scholar
  21. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). Logical Methods in Computer Science, 13(4), 2017. Google Scholar
  22. Evan Cavallo and Robert Harper. Higher Inductive Types in Cubical Computational Type Theory. Proc. ACM Program. Lang., 3(POPL):1:1-1:27, January 2019. URL: http://dx.doi.org/10.1145/3290314.
  23. James Chapman, Fredrik Nordvall Forsberg, and Conor McBride. The Box of Delights (Cubical Observational Type Theory), January 2018. Unpublished note. URL: https://github.com/msp-strath/platypus/blob/master/January18/doc/CubicalOTT/CubicalOTT.pdf.
  24. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. IfCoLog Journal of Logics and their Applications, 4(10):3127-3169, November 2017. URL: http://www.collegepublications.co.uk/journals/ifcolog/?00019.
  25. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., 1986. Google Scholar
  26. Thierry Coquand. Universe of Bishop sets, February 2017. URL: http://www.cse.chalmers.se/~coquand/bishop.pdf.
  27. Thierry Coquand. Canonicity and normalization for Dependent Type Theory, October 2018. URL: http://arxiv.org/abs/1810.09367.
  28. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264. ACM, 2018. URL: http://dx.doi.org/10.1145/3209108.3209197.
  29. 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, pages 120-134. Springer Berlin Heidelberg, 1996. Google Scholar
  30. Marcelo Fiore. Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus. In Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP '02, pages 26-37. ACM, 2002. URL: http://dx.doi.org/10.1145/571157.571161.
  31. Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, and Thorsten Altenkirch. Small Induction Recursion. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings, pages 156-172. Springer Berlin Heidelberg, 2013. Google Scholar
  32. Martin Hofmann. Extensional concepts in intensional type theory. phdthesis, University of Edinburgh, January 1995. Google Scholar
  33. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83-111. Oxford Univ. Press, 1998. Google Scholar
  34. Simon Huber. Canonicity for Cubical Type Theory. Journal of Automated Reasoning, June 2018. URL: http://dx.doi.org/10.1007/s10817-018-9469-1.
  35. Achim Jung and Jerzy Tiuryn. A new characterization of lambda definability. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, pages 245-257. Springer Berlin Heidelberg, 1993. Google Scholar
  36. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing Quotient Inductive-inductive Types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, January 2019. URL: http://dx.doi.org/10.1145/3290315.
  37. Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky), June 2016. Preprint. URL: http://arxiv.org/abs/1211.2851.
  38. Alexei Kopylov. Type Theoretical Foundations for Data Structures, Classes and Objects. phdthesis, Cornell University, 2004. Google Scholar
  39. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types, 2017. URL: http://arxiv.org/abs/1705.07088.
  40. Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009. Google Scholar
  41. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. Elsevier, 1975. URL: http://dx.doi.org/10.1016/S0049-237X(08)71945-1.
  42. Per Martin-Löf. Constructive Mathematics and Computer Programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, pages 153-175, August 1979. Published by North Holland, Amsterdam. 1982. Google Scholar
  43. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  44. Conor McBride. Dependently typed functional programs and their proofs. phdthesis, University of Edinburgh, 1999. Google Scholar
  45. Ieke Moerdijk and Erik Palmgren. Wellfounded trees in categories. Annals of Pure and Applied Logic, 104(1):189-218, 2000. Google Scholar
  46. Bengt Nordström, Kent Peterson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, 1990. Google Scholar
  47. Frank Pfenning. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS '01, pages 221-. IEEE Computer Society, 2001. URL: http://dl.acm.org/citation.cfm?id=871816.871845.
  48. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5):1203-1277, 2015. URL: http://dx.doi.org/10.1017/S0960129514000565.
  49. Jonathan Sterling. Algebraic Type Theory and Universe Hierarchies, December 2018. URL: http://arxiv.org/abs/1902.08848.
  50. Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality, 2019. Extended version. URL: http://arxiv.org/abs/1904.08562.
  51. Thomas Streicher. Semantics of Type Theory: Correctness, Completeness, and Independence Results. Birkhauser Boston Inc., 1991. Google Scholar
  52. Thomas Streicher. Investigations Into Intensional Type Theory. Habilitationsschrift, Universität München, 1994. Google Scholar
  53. Andrew Swan. Separating Path and Identity Types in Presheaf Models of Univalent Type Theory, 2018. URL: http://arxiv.org/abs/https://arxiv.org/abs/1808.00920.
  54. Paul Taylor. Practical Foundations of Mathematics. Cambridge studies in advanced mathematics. Cambridge University Press, 1999. Google Scholar
  55. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, 2013.
  56. Vladimir Voevodsky. A simple type system with two identity types, February 2013. Talk at Andre Joyal’s 70th birthday conference. (Slides available at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS_slides.pdf). URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf.
  57. Vladimir Voevodsky. Mathematical theory of type theories and the initiality conjecture, April 2016. Research proposal to the Templeton Foundation for 2016-2019, project description. URL: http://www.math.ias.edu/Voevodsky/other/Voevodsky%20Templeton%20proposal.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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