Cubical type theory is an extension of dependent type theory which allows to directly argue about n-dimensional cubes (points, lines, squares, cubes etc.). It is based on a model of dependent type theory in cubical sets given in a constructive metatheory. The type theory allows for new ways to reason about identity types, e.g., function extensionality as well as Voevodsky's Univalence Axiom are provable in the system.