2016/07/14 by Huber, Simon · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1607.04156
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.