Teoría de tipos homotópica

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.^[6][1] Originalmente, la semántica categórica de Awodey y Warren interpreta la equivalencia de tipos como la equivalencia homotópica entre espacios topológicos.^[2] Así, decimos que dos tipos son equivalentes, ${\displaystyle X\simeq Y}$ si existen dos funciones continuas ${\displaystyle f:X\rightarrow Y,\ g:Y\rightarrow X}$ tal que ${\displaystyle f\circ g\sim 1_{Y}}$ y ${\displaystyle g\circ f\sim 1_{X}}$, donde ${\displaystyle \phi \sim \psi }$ significa que ambas funciones son homotópicas, y donde ${\displaystyle 1_{X}}$ se entiende como el morfismo identidad de ${\displaystyle X}$, i.e. ${\displaystyle 1_{X}:X\rightarrow X}$ tal que ${\displaystyle 1_{X}(x)=x,\forall x:X.}$

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

${\displaystyle (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 en sí misma. Es decir, tenemos que

${\displaystyle (A=B)\simeq (A\simeq B).}$

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

Según Awodey,^[7] 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: ${\displaystyle f:X\rightarrow Y,\ g:Y\rightarrow X}$ tal que ${\displaystyle f\circ g=1_{Y}}$ y ${\displaystyle g\circ f=1_{X}}$. 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).^[8][1]

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:^[9][10][11]

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

Un fundamento autónomo es un fundamento formal, ${\displaystyle \Gamma }$, 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 siglo XX, como el fundamento tanto formal como autónomo estándar de las matemáticas modernas. Sin embargo, objetos como las ${\displaystyle (\infty ,1)}$-categorías, los ${\displaystyle (\infty ,1)}$-topos o los ${\displaystyle \infty }$-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.^{[12][13][14][15]} Por otro lado, Benacerraf (1965) argumenta que los números tampoco pueden ser conjuntos, según su famoso problema de identificación.^[16]

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.^[11][17] 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.^[18][19][20]

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.^{[21][22][10][8]}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, ${\displaystyle 0:\mathbb {N} }$ 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.^[23]

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.^[23]

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.^[24][25][26]