Cubical syntax for reflection-free extensional equality

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Jonathan Sterling, Carnegie Mellon University
  • ,
  • Carlo Angiuli, Carnegie Mellon University
  • ,
  • Daniel Gratzer

We contribute XTT, a cubical reconstruction of Observational Type Theory [7] 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 [27, 48]: every closed element of boolean type is derivably equal to either true or false.

Original languageEnglish
Title of host publication4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019
EditorsHerman Geuvers
Number of pages25
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication year2019
Article number31
ISBN (Electronic)9783959771078
DOIs
Publication statusPublished - 2019
Event4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019 - Dortmund, Germany
Duration: 24 Jun 201930 Jun 2019

Conference

Conference4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019
LandGermany
ByDortmund
Periode24/06/201930/06/2019
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume131
ISSN1868-8969

    Research areas

  • Canonicity, Categorical gluing, Cubical type theory, Dependent type theory, Extensional equality

See relations at Aarhus University Citationformats

ID: 159309906