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.​

Portada de Homotopy Type Theory: Univalent Foundations of Mathematics.

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

$(A=B)\to (A\simeq B),$

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

$(A=B)\simeq (A\simeq B).$

En otras palabras, la igualdad es equivalente a la equivalencia. Podemos considerar dos tipos equivalentes como iguales

Referencias

• Datos: Q5891840
• Multimedia: Homotopy type theory / Q5891840