(Joint work with Cyril Cohen, Thierry Coquand and Simon Huber)

Homotopy type theory is an extension of dependent type theory inspired by connections to abstract homotopy theory. This connection was discovered, among others, by Fields medalist Vladimir Voevodsky and from it a new axiom, called the univalence axiom, was added to type theory. This axiom provides extensionality principles, for instance function extensionality and the possibility to transport properties between isomorphic structures. One of the open problems in this new field is whether this axiom has computational content. In this talk I will discuss an extension to dependent type theory, called cubical type theory, which allows the user to directly argue about higher dimensional cubes representing equality proofs. This system provides new ways to reason about equality in type theory, in particular the univalence axiom is provable in the system which hence gives a computational justification for it.