An introduction to cubical type theory
- Date: Wednesday 22 November 2017, 14:00 – 15:00
- Location: Mathematics Level 8, MALL 2, School of Mathematics
- Type: Proofs, Constructions and Computations, Seminars, Pure Mathematics
- Cost: Free
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.