Cubical Syntax for Reflection-Free Extensional Equality
From MaRDI portal
Publication:6317399
DOI10.4230/LIPICS.FSCD.2019.31zbMATH Open1528.03113arXiv1904.08562MaRDI QIDQ6317399FDOQ6317399
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli
Publication date: 17 April 2019
Abstract: We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-L"of'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'.
This page was built for publication: Cubical Syntax for Reflection-Free Extensional Equality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6317399)
