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.
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
Escribe un comentario o lo que quieras sobre Teoría de tipos homotópica (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)