Canonicity for Cubical Type Theory

• DOI: 10.1007/s10817-018-9469-1
• Publication Date: 2018-06-13T03:13:16Z
• Authors: Simon Huber
• Keywords: Type theory; Argument (complex analysis)

Cubical type theory is an extension of Martin-Löf recently proposed by Cohen, Coquand, Mörtberg, and the author which allows for direct manipulation n-dimensional cubes where Voevodsky’s Univalence Axiom provable. In this paper we prove canonicity cubical theory: any natural number in a context build from only name variables judgmentally equal to numeral. To achieve formulate typed deterministic operational semantics employ computability argument adapted presheaf-like setting.