  This paper presents a type theory in which it is possible to directly
manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on
an interpretation of dependent type theory in a cubical set model. This enables
new ways to reason about identity types, for instance, function extensionality
is directly provable in the system. Further, Voevodsky's univalence axiom is
provable in this system. We also explain an extension with some higher
inductive types like the circle and propositional truncation. Finally we
provide semantics for this cubical type theory in a constructive meta-theory.
