Cubical Syntax for Reflection-Free Extensional Equality
arXiv:1904.08562 · doi:10.4230/LIPIcs.FSCD.2019.31
Abstract
We contribute XTT, a cubical reconstruction of Observational Type Theory 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 types 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 cubical extension (independently proposed by Awodey) of the logical families or categorical gluing argument inspired by Coquand and Shulman: every closed element of boolean type is derivably equal to either 'true' or 'false'.
arXiv commentExtended version; International Conference on Formal Structures for Computation and Deduction (FSCD), 2019
Cited by in corpus (6)
- Strategies, model checking and branching-time properties in Maude
- Normalization for Cubical Type Theory
- Model checking strategy-controlled systems in rewriting logic
- Decalf: A Directed, Effectful Cost-Aware Logical Framework
- A Cubical Language for Bishop Sets
- Logical Relations as Types: Proof-Relevant Parametricity for Program Modules