Canonicity for Cubical Type Theory
Journal of Automated Reasoning(2018)
摘要
Cubical type theory is an extension of Martin-Löf type theory recently proposed by Cohen, Coquand, Mörtberg, and the author which allows for direct manipulation of n -dimensional cubes and where Voevodsky’s Univalence Axiom is provable. In this paper we prove canonicity for cubical type theory: any natural number in a context build from only name variables is judgmentally equal to a numeral. To achieve this we formulate a typed and deterministic operational semantics and employ a computability argument adapted to a presheaf-like setting.
更多查看译文
关键词
Cubical type theory,Dependent type theory,Canonicity
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要