Teoría de tipos homotópica

En lógica matemática y ciencias de la computación, la teoría de tipos homotópica (HoTT /hɒt/, por sus siglas en inglés) son varias líneas de desarrollo de la teoría de tipos intensional, basada en interpretar los tipos como objetos a los cuales se aplican las intuiciones de la teoría de homotopía abstracta.

Al definir la noción de equivalencia en teoría de tipos homotópica, podemos notar que existe una forma canónica de convertir caminos en equivalencias; es decir, existe una función del tipo expresando que dos tipos A y B que son iguales son, en particular, equivalentes.

El axioma de univalencia declara que esta función que acabamos de definir es una equivalencia.

Es decir, tenemos que En otras palabras, la igualdad es equivalente a la equivalencia.

Podemos considerar dos tipos equivalentes como iguales