We present a dependent type theory organized around a Cartesian notion of cubes
(with faces, degeneracies, and diagonals), supporting both fibrant and
non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom
and includes a circle type, while the non-fibrant fragment includes exact (strict)
equality types satisfying equality reflection. Our type theory is defined by a
semantics in cubical partial equivalence relations, and is the first two-level
type theory to satisfy the canonicity property: all closed terms of boolean type
evaluate to either true or false.