A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic

Authors Robin Adams, Marc Bezem, Thierry Coquand

Thumbnail PDF


  • Filesize: 486 kB
  • 20 pages

Document Identifiers

Author Details

Robin Adams
Marc Bezem
Thierry Coquand

Cite AsGet BibTex

Robin Adams, Marc Bezem, and Thierry Coquand. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity - that every closed term computes to a canonical form. A computation becomes "stuck" when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension. As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Omega. There are proofs which inhabit propositions, which are the terms of type Omega. The canonical propositions are those constructed from false by implication. Thirdly, there are paths which inhabit equations M =_A N, where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality - logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
  • type theory
  • univalence
  • canonicity


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


  1. Carlo Angiuli, Robert Harper, and Todd Wilson. Computational higher-dimensional type theory. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 680-693. ACM, 2017. URL: http://dx.doi.org/10.1145/3093333.3009861.
  2. Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107-128, Dagstuhl, Germany, 2014. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2013.107.
  3. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. CoRR, abs/1611.02108, 2016. URL: http://arxiv.org/abs/1611.02108.
  4. Jean-Yves Girard. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  5. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  6. Simon Huber. Canonicity for cubical type theory. CoRR, abs/1607.04156, 2016. URL: http://arxiv.org/abs/1607.04156.
  7. Daniel R. Licata and Robert Harper. Canonicity for 2-dimensional type theory. In John Field and Michael Hicks, editors, POPL, pages 337-348. ACM, 2012. URL: http://dx.doi.org/10.1145/2103656.2103697.
  8. Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994. Google Scholar
  9. Andrew Polonsky. Internalization of extensional equality. CoRR, abs/1401.1148, 2014. URL: http://arxiv.org/abs/1401.1148.
  10. W. W. Tait. Intensional iinterpretation of ffunctional of finite type i. Journal of Symbolic Logic, 32:198-212, 1967. Google Scholar
  11. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail