En el Robert Harper curso en Homotopy Tipo de Teoría, habla acerca de cómo sería deseable encontrar un computacional interpretación de la Univalence Axioma, como podría ofrecer una manera de correr HoTT programas. En el tiempo (en 2013), este fue un problema abierto. Es todavía hoy un problema abierto? Si es así, ¿ expertos creen que una interpretación computacional se encuentra?
Al escribir esta pregunta, he encontrado este artículo por Cohen, Coquand, Huber y Mörtberg (2016); lo que dice
En este trabajo se presenta un tipo de teoría en la cual es posible manipular directamente de n-dimensiones de los cubos (puntos, líneas, cuadrados, cubos, etc.) basado en una interpretación de tipo dependiente de la teoría en una cúbica modelo de conjunto. Esto permite nuevas formas de la razón sobre los tipos de identidad, por ejemplo, la función extensionality es directamente comprobable en el sistema. Además, Voevodsky del univalence axioma es comprobable en este sistema. También explicamos una extensión con algunos de los más inductivo tipos como el círculo y proposicional de truncamiento. Finalmente ofrecemos una semántica para este cúbica tipo de teoría constructiva de la meta-teoría.
Quizás a la luz de esto, mi pregunta es trivial, pero mi undestanding de que el tema es muy limitada. Esto no significa que el problema ya está cerrado?
