Teoría de tipos de homotopía

En lógica matemática y ciencias de la computación , la teoría de tipos de homotopía ( HoTT ) se refiere a varias líneas de desarrollo de la teoría de tipos intuicionista , basada en la interpretación de los tipos como objetos a los que se aplica la intuición de la teoría de homotopía (abstracta) .

Esto incluye, entre otras líneas de trabajo, la construcción de modelos homotópicos y de categorías superiores para dichas teorías de tipos; el uso de la teoría de tipos como una lógica (o lenguaje interno ) para la teoría de homotopía abstracta y la teoría de categorías superiores ; el desarrollo de las matemáticas dentro de una base teórica de tipos (incluyendo tanto las matemáticas previamente existentes como las nuevas matemáticas que los tipos homotópicos hacen posibles); y la formalización de cada uno de estos en asistentes de prueba de computadora .

Existe una gran superposición entre el trabajo conocido como teoría de tipos de homotopía y el llamado proyecto de fundamentos univalentes . Aunque ninguno de los dos está delineado con precisión y los términos a veces se usan indistintamente, la elección del uso también corresponde a veces a diferencias de punto de vista y énfasis. ^[1] Por lo tanto, este artículo puede no representar las opiniones de todos los investigadores en los campos por igual. Este tipo de variabilidad es inevitable cuando un campo está en rápido cambio.

En un momento dado, la idea de que los tipos en la teoría de tipos intensionales con sus tipos identidad podían considerarse grupoides era un folclore matemático . Se precisó semánticamente por primera vez en el artículo de 1994 de Martin Hofmann y Thomas Streicher llamado "El modelo grupoide refuta la unicidad de las pruebas de identidad", ^[2] en el que demostraron que la teoría de tipos intensionales tenía un modelo en la categoría de grupoides . Este fue el primer modelo verdaderamente " homotópico " de la teoría de tipos, aunque solo "unidimensional " (los modelos tradicionales en la categoría de conjuntos son homotópicamente 0-dimensionales).

Su artículo de seguimiento ^[3] prefiguró varios desarrollos posteriores en la teoría de tipos de homotopía. Por ejemplo, observaron que el modelo de grupoide satisface una regla que llamaron "extensionalidad del universo", que no es otra que la restricción a los 1-tipos del axioma de univalencia que Vladimir Voevodsky propuso diez años después. (Sin embargo, el axioma para los 1-tipos es notablemente más simple de formular, ya que no se requiere una noción coherente de "equivalencia"). También definieron "categorías con isomorfismo como igualdad" y conjeturaron que en un modelo que use grupoides de dimensiones superiores, para tales categorías se tendría "equivalencia es igualdad"; esto fue demostrado más tarde por Benedikt Ahrens, Krzysztof Kapulkin y Michael Shulman . ^[4]

Los primeros modelos de dimensiones superiores de la teoría de tipos intensionales fueron construidos por Steve Awodey y su estudiante Michael Warren en 2005 utilizando las categorías de modelos de Quillen . Estos resultados se presentaron por primera vez en público en la conferencia FMCS 2006 ^[5] en la que Warren dio una charla titulada "Modelos de homotopía de la teoría de tipos intensionales", que también sirvió como prospecto de tesis (el comité de disertación presente fue Awodey, Nicola Gambino y Alex Simpson). Un resumen se incluye en el resumen del prospecto de tesis de Warren. ^[6]

En un taller posterior sobre tipos de identidad en la Universidad de Uppsala en 2006 ^[7] hubo dos charlas sobre la relación entre la teoría de tipos intensionales y los sistemas de factorización: una de Richard Garner, "Sistemas de factorización para la teoría de tipos", ^[8] y otra de Michael Warren, "Categorías de modelos y tipos de identidad intensionales". Se discutieron ideas relacionadas en las charlas de Steve Awodey, "Teoría de tipos de categorías de dimensiones superiores", y Thomas Streicher , "Tipos de identidad frente a grupoides omega débiles: algunas ideas, algunos problemas". En la misma conferencia, Benno van den Berg dio una charla titulada "Tipos como categorías omega débiles" donde esbozó las ideas que más tarde se convirtieron en el tema de un artículo conjunto con Richard Garner.

Todas las primeras construcciones de modelos de dimensiones superiores tuvieron que lidiar con el problema de la coherencia típico de los modelos de la teoría de tipos dependientes, y se desarrollaron varias soluciones. Una de ellas fue propuesta en 2009 por Voevodsky, otra en 2010 por van den Berg y Garner. ^[9] Una solución general, basada en la construcción de Voevodsky, fue finalmente propuesta por Lumsdaine y Warren en 2014. ^[10]

En el PSSL86 de 2007 ^[11], Awodey dio una charla titulada "Teoría de tipos de homotopía" (este fue el primer uso público de ese término, que fue acuñado por Awodey ^[12] ). Awodey y Warren resumieron sus resultados en el artículo "Modelos teóricos de homotopía de tipos de identidad", que se publicó en el servidor de preimpresión ArXiv en 2007 ^[13] y en 2009; una versión más detallada apareció en la tesis de Warren "Aspectos teóricos de homotopía de la teoría de tipos constructiva" en 2008.

Casi al mismo tiempo, Vladimir Voevodsky estaba investigando de forma independiente la teoría de tipos en el contexto de la búsqueda de un lenguaje para la formalización práctica de las matemáticas. En septiembre de 2006 publicó en la lista de correo Types "Una nota muy breve sobre el cálculo lambda de homotopía ", ^[14] que esbozaba los lineamientos de una teoría de tipos con productos, sumas y universos dependientes y de un modelo de esta teoría de tipos en conjuntos simpliciales Kan . Comenzaba diciendo "El cálculo lambda de homotopía es un sistema de tipos hipotético (por el momento)" y terminaba con "Por el momento, mucho de lo que dije anteriormente está en el nivel de conjeturas. Incluso la definición del modelo de TS en la categoría de homotopía no es trivial", haciendo referencia a los complejos problemas de coherencia que no se resolvieron hasta 2009. Esta nota incluía una definición sintáctica de los "tipos de igualdad" que se afirmaba que se interpretaban en el modelo mediante espacios de caminos, pero no consideraba las reglas de Per Martin-Löf para los tipos identidad. También estratificó los universos por dimensión de homotopía además del tamaño, una idea que luego fue prácticamente descartada.

En el aspecto sintáctico, Benno van den Berg conjeturó en 2006 que la torre de tipos identidad de un tipo en la teoría de tipos intensionales debería tener la estructura de una ω-categoría, y de hecho de un ω-grupoide, en el sentido "globular, algebraico" de Michael Batanin. Esto fue demostrado posteriormente de forma independiente por van den Berg y Garner en el artículo "Types are weak omega-groupoids" (publicado en 2008), ^[15] y por Peter Lumsdaine en el artículo "Weak ω-Categories from Intensional Type Theory" (publicado en 2009) y como parte de su tesis doctoral de 2010 "Higher Categories from Type Theories" (Categorías superiores a partir de teorías de tipos). ^[16]

El concepto de fibración univalente fue introducido por Voevodsky a principios de 2006. ^[17] Sin embargo, debido a la insistencia de todas las presentaciones de la teoría de tipos de Martin-Löf en la propiedad de que los tipos identidad, en el contexto vacío, pueden contener solo reflexividad, Voevodsky no reconoció hasta 2009 que estos tipos identidad pueden usarse en combinación con los universos univalentes. En particular, la idea de que la univalencia puede introducirse simplemente agregando un axioma a la teoría de tipos de Martin-Löf existente apareció recién en 2009. ^{[a] [b]}

También en 2009, Voevodsky elaboró ​​más detalles de un modelo de teoría de tipos en complejos Kan y observó que la existencia de una fibración Kan universal podría usarse para resolver los problemas de coherencia de los modelos categóricos de teoría de tipos. También demostró, usando una idea de AK Bousfield, que esta fibración universal era univalente: la fibración asociada de equivalencias de homotopía por pares entre las fibras es equivalente a la fibración del espacio de caminos de la base.

Para formular la univalencia como un axioma, Voevodsky encontró una forma de definir "equivalencias" sintácticamente que tenían la importante propiedad de que el tipo que representaba la afirmación "f es una equivalencia" era (bajo el supuesto de extensionalidad de la función) (-1)-truncado (es decir, contráctil si estaba habitado). Esto le permitió dar una afirmación sintáctica de univalencia, generalizando la "extensionalidad del universo" de Hofmann y Streicher a dimensiones superiores. También pudo usar estas definiciones de equivalencias y contractibilidad para comenzar a desarrollar cantidades significativas de "teoría de homotopía sintética" en el asistente de pruebas Coq ; esto formó la base de la biblioteca más tarde llamada "Foundations" y eventualmente "UniMath". ^[19]

La unificación de los distintos hilos comenzó en febrero de 2010 con una reunión informal en la Universidad Carnegie Mellon , donde Voevodsky presentó su modelo en complejos Kan y su Coq a un grupo que incluía a Awodey, Warren, Lumsdaine, Robert Harper , Dan Licata, Michael Shulman y otros. Esta reunión produjo los lineamientos de una prueba (por Warren, Lumsdaine, Licata y Shulman) de que cada equivalencia de homotopía es una equivalencia (en el buen sentido coherente de Voevodsky), basada en la idea de la teoría de categorías de mejorar las equivalencias a equivalencias adjuntas. Poco después, Voevodsky demostró que el axioma de univalencia implica extensionalidad de funciones.

El siguiente evento crucial fue un minitaller en el Instituto de Investigación Matemática de Oberwolfach en marzo de 2011 organizado por Steve Awodey, Richard Garner, Per Martin-Löf y Vladimir Voevodsky, titulado "La interpretación homotópica de la teoría de tipos constructivos". ^[20] Como parte de un tutorial de Coq para este taller, Andrej Bauer escribió una pequeña biblioteca de Coq ^[21] basada en las ideas de Voevodsky (pero sin usar realmente nada de su código); esto eventualmente se convirtió en el núcleo de la primera versión de la biblioteca de Coq "HoTT" ^[22] (la primera confirmación de esta última ^[23] por Michael Shulman señala "Desarrollo basado en los archivos de Andrej Bauer, con muchas ideas tomadas de los archivos de Vladimir Voevodsky"). Una de las cosas más importantes que surgieron de la reunión de Oberwolfach fue la idea básica de los tipos inductivos superiores, gracias a Lumsdaine, Shulman, Bauer y Warren. Los participantes también formularon una lista de preguntas abiertas importantes, como si el axioma de univalencia satisface la canonicidad (aún abierta, aunque algunos casos especiales se han resuelto positivamente ^{[24] [25]} ), si el axioma de univalencia tiene modelos no estándar (desde entonces respondido positivamente por Shulman), y cómo definir tipos (semi)simpliciales (aún abierta en MLTT, aunque se puede hacer en el Sistema de Tipos de Homotopía (HTS) de Voevodsky, una teoría de tipos con dos tipos de igualdad).

Poco después del taller de Oberwolfach, se creó el sitio web y el blog Homotopy Type Theory ^[26] , y el tema comenzó a popularizarse bajo ese nombre. Se puede obtener una idea de algunos de los avances importantes durante este período a partir de la historia del blog. ^[27]

La frase "fundamentos univalentes" está estrechamente relacionada con la teoría de tipos homotópicos, pero no todos la utilizan de la misma manera. Originalmente, Vladimir Voevodsky la utilizó para referirse a su visión de un sistema fundacional para las matemáticas en el que los objetos básicos son tipos homotópicos, basados ​​en una teoría de tipos que satisface el axioma de univalencia y formalizada en un asistente de prueba computacional. ^[28]

A medida que el trabajo de Voevodsky se fue integrando con la comunidad de otros investigadores que trabajaban en la teoría de tipos de homotopía, "fundamentos univalentes" se usó a veces indistintamente con "teoría de tipos de homotopía", ^[29] y otras veces para referirse solo a su uso como un sistema fundacional (excluyendo, por ejemplo, el estudio de la semántica de categorías de modelos o la metateoría computacional). ^[30] Por ejemplo, el tema del año especial del IAS se dio oficialmente como "fundamentos univalentes", aunque gran parte del trabajo realizado allí se centró en la semántica y la metateoría además de los fundamentos. El libro producido por los participantes en el programa del IAS se tituló "Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas"; aunque esto podría referirse a cualquiera de los dos usos, ya que el libro solo analiza HoTT como fundamento matemático. ^[29]

En 2012-13, los investigadores del Instituto de Estudios Avanzados organizaron "Un año especial sobre fundamentos univalentes de las matemáticas". ^[31] El año especial reunió a investigadores en topología , informática , teoría de categorías y lógica matemática . El programa fue organizado por Steve Awodey , Thierry Coquand y Vladimir Voevodsky .

Durante el programa, Peter Aczel , uno de los participantes, inició un grupo de trabajo que investigó cómo hacer teoría de tipos de manera informal pero rigurosa, en un estilo análogo al de los matemáticos ordinarios que hacen teoría de conjuntos. Después de los experimentos iniciales, quedó claro que esto no solo era posible sino altamente beneficioso, y que se podía y debía escribir un libro (el llamado HoTT Book ) ^{[29] [32]} . Muchos otros participantes del proyecto se unieron al esfuerzo con apoyo técnico, redacción, corrección de pruebas y aportando ideas. Inusualmente para un texto de matemáticas, se desarrolló de manera colaborativa y abierta en GitHub , se publica bajo una licencia Creative Commons que permite a las personas crear su propia versión del libro y se puede comprar en forma impresa y descargar de forma gratuita. ^{[33] [34] [35]}

De manera más general, el año especial fue un catalizador para el desarrollo de todo el tema; el Libro HoTT fue sólo uno de los resultados, aunque el más visible.

Participantes oficiales del año especial

ACM Computing Reviews incluyó el libro como una publicación destacada de 2013 en la categoría "matemáticas de la computación". ^[36]

HoTT utiliza una versión modificada de la interpretación de la teoría de tipos según la cual los tipos también pueden representar proposiciones y los términos pueden representar pruebas. Sin embargo, en HoTT, a diferencia de las "proposiciones como tipos" estándar, las "meras proposiciones" desempeñan un papel especial, que, en términos generales, son aquellos tipos que tienen como máximo un término, hasta la igualdad proposicional . Se parecen más a las proposiciones lógicas convencionales que a los tipos generales, en el sentido de que no son relevantes para las pruebas.

El concepto fundamental de la teoría de tipos de homotopía es el camino . En HoTT, el tipo es el tipo de todos los caminos desde el punto hasta el punto . (Por lo tanto, una prueba de que un punto es igual a un punto es lo mismo que un camino desde el punto hasta el punto .) Para cualquier punto , existe un camino de tipo , que corresponde a la propiedad reflexiva de igualdad. Un camino de tipo se puede invertir, formando un camino de tipo , que corresponde a la propiedad simétrica de igualdad. Dos caminos de tipo respectivamente se pueden concatenar, formando un camino de tipo ; esto corresponde a la propiedad transitiva de igualdad. ${\estilo de visualización a=b}$${\estilo de visualización a}$${\estilo de visualización b}$${\estilo de visualización a}$${\estilo de visualización b}$${\estilo de visualización a}$${\estilo de visualización b}$${\estilo de visualización a}$${\displaystyle a=a}$${\estilo de visualización a=b}$${\displaystyle b=a}$${\estilo de visualización a=b}$${\estilo de visualización b=c}$${\estilo de visualización a=c}$

Lo más importante es que, dada una ruta y una prueba de alguna propiedad , la prueba puede "transportarse" a lo largo de la ruta para producir una prueba de la propiedad . (En otras palabras, un objeto de tipo puede convertirse en un objeto de tipo ). Esto corresponde a la propiedad de sustitución de igualdad . Aquí entra en juego una diferencia importante entre HoTT y las matemáticas clásicas. En las matemáticas clásicas, una vez que se ha establecido la igualdad de dos valores y , y pueden usarse indistintamente a partir de entonces, sin tener en cuenta ninguna distinción entre ellos. Sin embargo, en la teoría de tipos de homotopía, puede haber múltiples rutas diferentes , y transportar un objeto a lo largo de dos rutas diferentes producirá dos resultados diferentes. Por lo tanto, en la teoría de tipos de homotopía, al aplicar la propiedad de sustitución, es necesario indicar qué ruta se está utilizando. ${\displaystyle p:a=b}$${\displaystyle P(a)}$${\estilo de visualización p}$${\estilo de visualización P(b)}$${\displaystyle P(a)}$${\estilo de visualización P(b)}$${\estilo de visualización a}$${\estilo de visualización b}$${\estilo de visualización a}$${\estilo de visualización b}$${\estilo de visualización a=b}$

En general, una "proposición" puede tener múltiples demostraciones diferentes. (Por ejemplo, el tipo de todos los números naturales, cuando se considera como una proposición, tiene a cada número natural como demostración). Incluso si una proposición tiene solo una demostración , el espacio de caminos puede ser no trivial de alguna manera. Una "mera proposición" es cualquier tipo que esté vacío o que contenga solo un punto con un espacio de caminos trivial . ${\estilo de visualización a}$${\displaystyle a=a}$

Tenga en cuenta que la gente escribe para , por lo que deja implícito el tipo de . No lo confunda con , que denota la función identidad en . ^[c]${\estilo de visualización a=b}$$Estilo de visualización Id_{A}(a,b)}$${\estilo de visualización A}$${\estilo de visualización a,b}$${\displaystyle id_{A}:A\to A}$${\estilo de visualización A}$

Dos tipos y pertenencia a un universo se definen como equivalentes si existe una equivalencia entre ellos. Una equivalencia es una función ${\estilo de visualización A}$${\estilo de visualización B}$${\estilo de visualización U}$

${\displaystyle f:A\to B}$

que tiene tanto una inversa izquierda como una inversa derecha, en el sentido de que para y adecuadamente elegidos , los siguientes tipos están habitados: ${\estilo de visualización g}$${\estilo de visualización h}$

${\displaystyle Id_{B\rightarrow B}(f\circ g,id_{B}),}$

${\displaystyle Id_{A\rightarrow A}(h\circ f,id_{A}).}$

es decir

${\displaystyle f\circ g=_{B\rightarrow B}id_{B},}$

${\displaystyle h\circ f=_{A\rightarrow A}id_{A}.}$

Esto expresa una noción general de " tiene tanto una inversa izquierda como una inversa derecha", utilizando tipos de igualdad. Nótese que las condiciones de invertibilidad anteriores son tipos de igualdad en los tipos de función y . En general, se asume el axioma de extensionalidad de la función, que garantiza que estos son equivalentes a los siguientes tipos que expresan invertibilidad utilizando la igualdad en el dominio y codominio y : ${\estilo de visualización f}$${\displaystyle A\flecha derecha A}$${\displaystyle B\flecha derecha B}$${\estilo de visualización A}$${\estilo de visualización B}$

${\displaystyle \Pi _{y:B}.\ Id_{B}((f\circ g)(y),id_{B}(y)),}$

${\displaystyle \Pi_{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).}$

es decir para todos y , ${\estilo de visualización x:A}$${\estilo de visualización y:B}$

${\displaystyle f(g(y))=_{B}y,}$

${\displaystyle h(f(x))=_{A}x.}$

Las funciones del tipo

${\displaystyle A\to B}$

junto con una prueba de que son equivalencias se denotan por

${\displaystyle A\simeq B}$.

Habiendo definido funciones que son equivalencias como las anteriores, se puede demostrar que existe una forma canónica de convertir caminos en equivalencias. En otras palabras, existe una función del tipo

${\displaystyle (A=B)\to (A\simeq B),}$

lo que expresa que los tipos que son iguales son, en particular, también equivalentes. ${\estilo de visualización A,B}$

El axioma de univalencia establece que esta función es en sí misma una equivalencia. ^{[29] : 115  [18] : 4–6} Por lo tanto, tenemos

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

"En otras palabras, la identidad es equivalente a la equivalencia. En particular, se puede decir que 'los tipos equivalentes son idénticos'". ^{[29] : 4}

Martín Hötzel Escardó ha demostrado que la propiedad de univalencia es independiente de la teoría de tipos de Martin-Löf (MLTT). ^{[18] : 6  [d]}

Los defensores de HoTT afirman que permite traducir las pruebas matemáticas a un lenguaje de programación informática para los asistentes de pruebas informáticas con mucha más facilidad que antes. Argumentan que este enfoque aumenta la posibilidad de que las computadoras comprueben pruebas difíciles. ^[37] Sin embargo, estas afirmaciones no son aceptadas universalmente y muchos esfuerzos de investigación y asistentes de pruebas no hacen uso de HoTT.

HoTT adopta el axioma de univalencia, que relaciona la igualdad de proposiciones lógico-matemáticas con la teoría de homotopía. Una ecuación como es una proposición matemática en la que dos símbolos diferentes tienen el mismo valor. En la teoría de tipos de homotopía, esto se entiende como que las dos formas que representan los valores de los símbolos son topológicamente equivalentes. ^[37]${\estilo de visualización a=b}$

Según Giovanni Felder , director del Instituto de Estudios Teóricos de la ETH de Zúrich , estas relaciones de equivalencia se pueden formular mejor en la teoría de la homotopía porque es más completa: la teoría de la homotopía no sólo explica por qué "a es igual a b", sino también cómo derivarlo. En la teoría de conjuntos, esta información tendría que definirse adicionalmente, lo que, según sostienen sus defensores, dificulta la traducción de proposiciones matemáticas a lenguajes de programación. ^[37]

A partir de 2015, se estaba realizando un intenso trabajo de investigación para modelar y analizar formalmente el comportamiento computacional del axioma de univalencia en la teoría de tipos de homotopía. ^[38]

La teoría de tipos cúbicos es un intento de dar contenido computacional a la teoría de tipos de homotopía. ^[39]

Sin embargo, se cree que ciertos objetos, como los tipos semi-simpliaces, no pueden construirse sin hacer referencia a alguna noción de igualdad exacta. Por lo tanto, se han desarrollado varias teorías de tipos de dos niveles que dividen sus tipos en tipos fibrantes, que respetan caminos, y tipos no fibrantes, que no los respetan. La teoría de tipos computacionales cúbicos cartesianos es la primera teoría de tipos de dos niveles que da una interpretación computacional completa a la teoría de tipos de homotopía. ^[40]

• Cálculo de construcciones
• Correspondencia entre Curry y Howard
• Teoría de tipos intuicionista
• Hipótesis de homotopía
• Fundaciones univalentes

• David Corfield (2020), Teoría de tipos de homotopía modal: la perspectiva de una nueva lógica para la filosofía , Oxford University Press.
• Egbert Rijke (2022), Introducción a la teoría de tipos de homotopía , arXiv :2212.11082. Libro de texto introductorio.

• Teoría de tipos de homotopía
• Teoría de tipos de homotopía en el laboratorio n
• Wiki de teoría de tipos de homotopía
• Página web de Vladimir Voevodsky sobre los fundamentos univalentes
• La teoría de tipos de homotopía y los fundamentos univalentes de las matemáticas por Steve Awodey
• "Teoría de tipos constructivos y homotopía": videoconferencia de Steve Awodey en el Instituto de Estudios Avanzados