miniaturadeimagen|Portada de Homotopy Type Theory: Univalent Foundations of Mathematics. En lógica matemática y ciencias de la computación, la teoría homotópica de tipos (HoTT /hɒt/, por sus siglas en inglés) son varias líneas de desarrollo de la Teoría de Tipos Dependientes, 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 usando las categorías de modelos de Quillen para teorías de tipos categóricas (o categorías cartesianas cerradas); 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 las matemáticas dentro de fundamentos basados 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.

Introducción Intuitivamente, la teoría homotópica de tipos (HoTT) interpreta la teoría de tipos de Martin-Löf de forma tal que cada tipo es un espacio topológico y cada término de un tipo es un punto en tal espacio. Formalmente, Awodey y Warren introducen por primera vez el modelo homotópico utilizando las categorías de modelos de Quillen, demostrando que estas categorías, así como las categorías simpliciales o las categorías de espacios topológicos, tienen una teoría de tipos de Martin-Löf como lenguaje interno.

HoTT extiende la teoría de tipos de Martin-Löf usando conceptos de teoría homotópica y añadiendo axiomas poco comunes como el axioma de Univalencia. Además, el concepto de identidad se relaja totalmente, en tanto la identidad entre términos de un tipo se entiende como un camino entre puntos de un espacio .

Para hablar de identidad de tipos, pueden agregarse universos a la teoría de tipos de Martin-Löf. La forma más usual es la jerarquía de Russell. Tendremos una jerarquía de universos que contienen al anterior y están cerrados bajo constructores de tipos:

Así, podemos hablar de identidad entre tipos, , para algún universo . La identidad entre tipos, es decir, un camino entre espacios, pueden interpretarse gracias al axioma de Univalencia que afirma que la identidad entre tipos es equivalente a la equivalencia entre tipos.

Axioma de Univalencia La noción de equivalencia de tipos en HoTT puede definirse de muchas formas lógicamente equivalentes que, sin embargo, son muy distintas como tipos. Originalmente, la semántica categórica de Awodey y Warren interpreta la equivalencia de tipos como la equivalencia homotópica entre espacios topológicos. Así, decimos que dos tipos son equivalentes, si existen dos funciones continuas tal que y , donde significa que ambas funciones son homotópicas, y donde se entiende como el morfismo identidad de , i.e. tal que

Al definir la noción de equivalencia, 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 en sí misma. Es decir, tenemos que

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

Según Awodey, esto implica que el axioma de Univalencia refleja la práctica estructuralista de considerar objetos isomórficos como idénticos, ya que un isomorfismo se define de forma análoga a la equivalencia homotópica: tal que y . Sin embargo, no es claro que la definición de isomorfismo de tipos en HoTT pueda ser compatible con el axioma de Univalencia, como discuten James Ladyman y Stuart Presnell (2019).

HoTT como fundamento autónomo Ya que la teoría de tipos de Martin-Löf es suficientemente expresiva para desarrollar una lógica intuicionista, teoría de conjuntos, teoría de homotopía o teoría de categorías, HoTT se ha propuesto como un fundamento para la totalidad de las matemáticas.

Podemos distinguir dos nociones relevantes a la hora de hablar de un fundamento matemático:

Un fundamento formal, , es tal que el resto de teorías matemáticas pueden desarrollarse usando los objetos, axiomas y reglas de inferencia de .

Un fundamento autónomo es un fundamento formal, , con una interpretación intuitiva o prematemática, i.e. no depende de otros conceptos matemáticos ya desarrollados.

La teoría de conjuntos de Zermelo-Fraenkel ha sido considerada, durante el , como el fundamento tanto formal como autónomo estándar de las matemáticas modernas. Sin embargo, objetos como las -categorías, los -topos o los -grupoides, que son parte de recientes desarrollos en teoría de categorías de mayor orden y teoría de homotopía, no pueden pensarse realmente como conjuntos. Por otro lado, Benacerraf (1965) argumenta que los números tampoco pueden ser conjuntos, según su famoso problema de identificación.

Estos resultados, junto con el estructuralismo predominante en la filosofía como práctica matemática, han llevado a reconsiderar el uso de ZFC como fundamento, presentando tentativamente a la teoría de categorías como fundamento estructuralista. Es aquí donde HoTT se presenta como un candidato a un fundamento de las matemáticas que, según algunos autores, sería también de corte estructuralista.

Para HoTT poder servir este rol, debe antes ser un fundamento autónomo. El primer proyecto para dar un fundamento autónomo a HoTT fue dado por James Ladyman y Stuart Presnell en una serie de varios artículos.En estos artículos, ambos autores desarrollan la idea de interpretar los tipos como conceptos. Estrictamente, los términos de cada tipo se interpretan como conceptos particulares qua conceptos generales, i.e. cada término es un concepto particular que instancia el concepto general de su tipo.

Por ejemplo, significa que el concepto particular de ser cero instancia el concepto general de ser un natural.

Aunque Ladyman y Presnell no son muy precisos, se entiende que su interpretación de los constructores de tipos es similar a la correspondencia Curry-Howard, en tanto afirman que: "las formas básicas en que los conceptos generales de las matemáticas pueden ser manipulados y combinados deben, por tanto, incluir aquellas descritas en la interpretación BHK de la lógica constructiva." (Ladyman & Presnell, 2018, p. 25)

Sin embargo, esta interpretación de los constructores, junto con otros principios que parecen intuitivos acerca de los conceptos generales, Bentzen (2020) logra derivar la regla del tercer excluso, la cual es inconsistente con el axioma de Univalencia.

Ladyman y Presnell también retoman el argumento fallido de Awodey (2018) para justificar el axioma de Univalencia usando su interpretación de tipos-como-conceptos. Para hacerlo, interpretan los universos de tipos como dominios de discurso. En este sentido, están determinados totalmente por sus elementos, i.e. extensionalmente.

Sin embargo, Ladyman y Presnell, manteniendo el espíritu intuicionista e intensional de la teoría de tipos de Martin-Löf, afirman que los tipos están totalmente caracterizados por su sentido, i.e. intensionalmente. Así, dos conceptos vacíos pueden ser distintos (como un triángulo de 5 lados y un círculo cuadrado). Pero en tanto los universos son a su vez tipos, parece contradictorio que estos tengan un carácter extensional mientras los tipos son intensionales. Así, Bentzen (2020) afirma que su acercamiento a la Univalencia no está bien fundado, pues los autores no logran responder satisfactoriamente a esta contradicción.

Otras aproximaciones a un fundamento autónomo para HoTT son aquellas de Tsementzis (2020), usando nociones espaciales y geométricas, o aquella de Bentzen (2021) usando la teoría cúbica de tipos, en la cual la Univalencia no es un axioma sino un teorema. Referencias

Categoría:Métodos formales Categoría:Teoría de tipos Categoría:Equivalencia (matemáticas)