¿Progreso hacia una interpretación computacional del axioma de univalencia?

Question

Voy a comenzar diciendo que no soy un experto en teoría de tipos. Sólo soy un curioso que se abre camino lentamente a través del libro HoTT cuando (raramente) tengo algo de tiempo libre.

Tengo curiosidad por saber si ha habido algún progreso hacia una interpretación computacional de la univalencia. Si no es así, ¿el sentimiento general es que la univalencia no es compatible con la computación?

Answer 1

Teoría de tipos cúbicos es una variante de la teoría de tipos que tiene todas las propiedades computacionales habituales (y algunas no habituales), y el Axioma de Univalencia es un teorema de la teoría de tipos cúbica. Como ya se ha señalado en los comentarios, existen implementaciones de la teoría de tipos cúbica con las que se puede jugar (incluso durante 90 horas).