  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.
