Canonicity for Cubical Type Theory

TL;DR

This paper proves canonicity for cubical type theory, showing that natural numbers in a context are judgmentally equal to numerals, using a typed operational semantics and a computability argument.

Contribution

It establishes the canonicity property for cubical type theory, a key step in understanding its computational behavior.

Findings

Any natural number in a context is judgmentally equal to a numeral.

The paper formulates a typed, deterministic operational semantics.

Employs a computability argument in a presheaf-like setting.

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 $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.