文章基本信息

标题：Cubical Syntax for Reflection-Free Extensional Equality
本地全文：下载
作者：Jonathan Sterling ; Carlo Angiuli ; Daniel Gratzer 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：131
页码：1-25
DOI：10.4230/LIPIcs.FSCD.2019.31
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Dependent type theory; extensional equality; cubical type theory; categorical gluing; canonicity