Canonicity for Cubical Type Theory
Logic in Computer Science
2017-10-31 v2
Abstract
Cubical type theory is an extension of Martin-L\"of type theory recently proposed by Cohen, Coquand, M\"ortberg and the author which allows for direct manipulation of -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.
Keywords
Cite
@article{arxiv.1607.04156,
title = {Canonicity for Cubical Type Theory},
author = {Simon Huber},
journal= {arXiv preprint arXiv:1607.04156},
year = {2017}
}
Comments
34 pages. v2: Added section on propositional truncation; fixed typos. To appear in the Journal of Automated Reasoning