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.

Esto incluye, entre otras líneas de trabajo, la construcción de modelos homotópicos y en teorías de categorías de alto orden para las teorías de tipos intensionales; el uso de la teoría de tipos como lógica (o lenguaje interno) de la teoría de homotopía abstracta y teoría de categorías de orden superior; el desarrollo de matemáticas dentro de  fundaciones basadas en teoría de tipos (incluyendo tanto matemática existente como la matemática nueva que los tipos homotópicos hacen posible); y la formalización de cada una de estas líneas en asistentes de demostración.

Axioma de univalencia 
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

Referencias 

Métodos formales
Teoría de tipos
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 . Esto incluye , entre otras líneas de trabajo , la construcción de modelos homotópicos y en teorías de categorías de alto orden para las teorías de tipos intensionales ; el uso de la teoría de tipos como lógica ( o lenguaje interno ) de la teoría de homotopía abstracta y teoría de categorías de orden superior ; el desarrollo de matemáticas dentro de fundaciones basadas en teoría de tipos ( incluyendo tanto matemática existente como la matemática nueva que los tipos homotópicos hacen posible ) ; y la formalización de cada una de estas líneas en asistentes de demostración . Axioma de univalencia 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 Referencias Métodos formales Teoría de tipos