An introduction to cubical type theory

Nicola Gambino, University of Leeds. Part of the PCC seminar series

Abstract: The rules of Martin-L\”of type theories are designed so as to ensure good proof-theoretical properties, such as normalization  (i.e. that every term reduces to one in canonical form), which can be  destroyed by the addition of axioms, such as Voevodsky’s univalence axiom. Coquand and his collaborators have introduced a novel  type theory, called cubical type theory, which remedies this situation  by having a new type constructor, called glueing, which makes the  univalence axiom provable. I will give an introduction to cubical type theory, explaining the most complex aspects of its  syntax by describing their semantical counterparts. The talk is based on  the paper “Cubical type theory: a computational interpretation of the  univalence axiom” by C. Cohen, T. Coquand, S. Huber and A. M\”ortberg.