Teoría de tipos homotópica y el axioma de univalencia

Antes que nada, me disculpo por la larga ausencia en el blog. Voy a tratar de comentarles, en este post, sobre un área reciente en teoría de tipos, en la cual me estoy empezando a interesar. No soy experto en el área, así que si hay alguien trabajando en esto, está más que invitado a postear en el blog. En este post sólo comento algunas ideas básicas, y porqué de mi repentino interés en esta teoría.

La teoría de tipos homotópica (o "HoTT" por sus siglas en inglés), es una nueva manera de interpretar la teoría de tipos. Empecemos con algunos conceptos básicos. De la wikipedia:

"En topología, y más precisamente en topología algebraica, dos aplicaciones continuas de un espacio topológico en otro se dicen homotópicas (del griego homos = mismo y topos = lugar) si una de ellas puede "deformarse continuamente" en la otra." -- Wikipedia: Homotopía

En teoría de tipos, se dice que dos tipos son isomorfos si hay una biyección entre ellos: o sea, A≡B si existen f:A→B y g:B→A tal que f∘g=id_B y g∘f = id_A. La idea de la teoría de tipos homotópica es considerar a los tipos A como espacio topológicos, los términos a como puntos en ese espacio, entonces a:A se traduce como a∈A. Una prueba de igualdad de dos términos de tipo A, es simplemente un camino de un punto a otro en ese espacio. Y finalmente una prueba de igualdad entre dos pruebas de igualdad, se interpreta como una homotopía. 

HoTT está planteado con tipos dependientes, donde existe el tipo Id_A(a,b), y una prueba con ese tipo es una prueba de que a=b en A. Pero como Id_A(a,b) en sí es un tipo, podemos probar que p=q en el tipo Id_A(a,b), o sea, podemos probar Id_(Id_A(a,b))(p,q), lo cual significa probar que dos pruebas de igualdad de a y b en el tipo A, son iguales. A eso es a lo que se considerará una homotopía en la interpretación HoTT.

Resumiendo:

Teoría de tipos	Teoría de homotopías
tipo A	espacio A
término a	punto a
a:A	a∈A
p:Id_A(a,b)	camino p:a↦b
g:Id_(Id_A(a,b))(p,q)	homotopía g:p⇒q

En particular, en tipos dependientes, los tipos son elementos de un tipo universal U (en realidad, existen diversos U para eliminar paradojas al estilo la de Russell, pero mantengamos la descripción simple). Por lo tanto, se puede probar también que dos tipos son iguales: Id_U(A,B).

Lo interesante del tema: el axioma de univalencia. El axioma es muy simple de escribir, pero tiene grandes implicaciones:  A~B ↔ A=B. O sea, si A y B son equivalentes/homotópicos, entonces A es igual a B (el sentido inverso de la flecha es trivial). O de otra manera, si dos tipos son equivalentes, entonces son iguales.

De dónde nació mi interés en el tema? Yo he estado trabajando en una teoría de tipos simple, módulo isomorfismos: es decir, si dos tipos son isomorfos, en esta teoría se consideran iguales (la versión más actualizada de este paper se encuentra en mi página web). Nuestro trabajo es una interpretación computacional: definimos el cálculo sintácticamente, y mostramos sus propiedades. Claro que no es tan sencillo en HoTT: nosotros usamos tipos simples, HoTT usa tipos dependientes. Nosotros sólo usamos dos conectivos: implicación y conjunción. En ese caso con sólo esos conectivos, sólo existen 4 isomorfismos a considerar. En HoTT, con tipos dependientes, hay que considerar todas las pruebas que se pueden realizar de igualdad. O sea: nuestro trabajo está muy lejos del tema HoTT... pero nos interesa ir hacia allí! Quizá algunas técnicas en nuestro trabajo puedan servir para la teoría de tipos homotópica, y es una dirección que estamos dispuestos a seguir.

A quienes les interese aprender sobre la teoría de tipos homotópica, existe un libro, el cual puede ser descargado gratuitamente de aquí, que es el libro que inició todo. La historia es así: Vladimir Voevodsky es el padre de ésta área, y muy pronto, gente muy reconocida empezó a involucrarse. En 2012-2013, el Institut for Advanced Studies de Princeton organizó un año de trabajo intensivo en ésta nueva área, y de allí salió el libro, que hoy se sigue modificando colaborativamente.

Para quienes se pregunten que tiene que ver todo esto con computación cuántica: pues nada. Yo comenzé con cuántica, me interesé por los tipos vectoriales, como una generalización de cuántica, y el no-determinismo en particular, los cuales me llevaron a los isomorfismos de tipos, a los cuales llegué desde cuántica y ahora me estoy interesando por esta nueva teoría a la cual llegué desde los tipos isomorfos. Sin embargo, hay un hilo conductor, por lo que algunas ideas de cuántica terminan colándose en los otros trabajos, y viceversa.