Apparaît dans la collection : 2014 - T2 - Semantics of proofs and certified mathematics

One of the key problems of Homotopy Type Theory is that it introduces axioms such as extensionality and univalence for which there is no known computational interpretation. We propose to overcome this by introducing a Type Theory where a heterogenous equality is defined recursively and equality for the universe just is univalence. This cubical type theory is inspired by Bernardy and Moulin's internal parametricity and by Coquand, Bezem and Huber's cubical set model. This is ongoing work with Ambrus Kaposi at Nottingham.