Teoría del tipo de homotopía - Homotopy type theory

Portada de la Teoría del Tipo de Homotopía: Fundamentos Univalentes de las Matemáticas .

En lógica matemática e informática , la teoría de tipos de homotopía ( HoTT / h ɒ t / ) se refiere a varias líneas de desarrollo de la teoría de tipos intuicionista , basada en la interpretación de 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 este tipo de teorías; el uso de la teoría de tipos como 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 (incluidas las matemáticas previamente existentes y las matemáticas nuevas que los tipos homotópicos hacen posibles); y la formalización de cada uno de estos en asistentes informáticos .

Existe una gran superposición entre el trabajo denominado teoría de tipos de homotopía y el proyecto de fundaciones univalentes . Aunque ninguno está delineado con precisión, y los términos a veces se usan indistintamente, la elección del uso también a veces corresponde a diferencias en el punto de vista y el énfasis. Como tal, es posible que este artículo no represente por igual las opiniones de todos los investigadores en los campos. Este tipo de variabilidad es inevitable cuando un campo está en rápido flujo.

Historia

Prehistoria: el modelo grupoide

En un momento, la idea de que los tipos en la teoría de tipos intensional con sus tipos de identidad podían considerarse grupoides era el folclore matemático . Primero se precisó semánticamente en el artículo de 1998 de Martin Hofmann y Thomas Streicher llamado "La interpretación grupoide de la teoría de tipos", en el que demostraron que la teoría de tipos intensional 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 sólo " unidimensional " (los modelos tradicionales en la categoría de conjuntos son homotópicamente 0-dimensionales).

Su artículo también presagió varios desarrollos posteriores en la teoría de tipos de homotopía. Por ejemplo, señalaron que el modelo grupoide satisface una regla que llamaron "extensionalidad del universo", que no es otra que la restricción a los tipos 1 del axioma de univalencia que Vladimir Voevodsky propuso diez años después. (El axioma para los tipos 1 es notablemente más simple de formular, sin embargo, 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 utiliza agrupaciones de dimensiones superiores, para tales categorías uno tendría "la equivalencia es la igualdad"; esto fue probado más tarde por Benedikt Ahrens, Krzysztof Kapulkin y Michael Shulman .

Historia temprana: categorías de modelos y grupoides superiores

Los primeros modelos de dimensión superior de la teoría de tipos intensionales fueron construidos por Steve Awodey y su alumno Michael Warren en 2005 utilizando categorías de modelos de Quillen . Estos resultados se presentaron por primera vez en público en la conferencia FMCS 2006 en la que Warren pronunció una charla titulada "Modelos de homotopía de la teoría de tipo intensional", que también le sirvió como prospecto de tesis (el comité de disertación presente fueron Awodey, Nicola Gambino y Alex Simpson). Un resumen está contenido en el resumen del prospecto de tesis de Warren.

En un taller posterior sobre tipos de identidad en la Universidad de Uppsala en 2006 hubo dos charlas sobre la relación entre la teoría de tipos intensional y los sistemas de factorización: una de Richard Garner, "Sistemas de factorización para la teoría de tipos", y otra de Michael Warren, "Categorías de modelos y tipos de identidad intensional ". Las ideas relacionadas fueron discutidas en las charlas de Steve Awodey, "Teoría de tipos de categorías de dimensiones superiores", y Thomas Streicher , "Tipos de identidad vs. omega-grupoides 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 describió las ideas que luego se convirtieron en el tema de un artículo conjunto con Richard Garner.

Todas las primeras construcciones de modelos de dimensiones superiores tenían que abordar el problema de coherencia típico de los modelos de la teoría de tipos dependientes, y se desarrollaron varias soluciones. Uno de ellos fue dado en 2009 por Voevodsky, otro en 2010 por van den Berg y Garner. Lumsdaine y Warren finalmente dieron una solución general, basada en la construcción de Voevodsky, en 2014.

En el PSSL86 en 2007, 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). 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 y en 2009; una versión más detallada apareció en la tesis de Warren "Aspectos teóricos de la homotopía de la teoría de tipos constructivos" en 2008.

Aproximadamente 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 de tipos "Una nota muy breve sobre el cálculo lambda de homotopía ", que esbozaba los contornos de una teoría de tipos con productos dependientes, sumas y universos y de un modelo de este tipo de teoría en conjuntos simpliciales Kan . Comenzó diciendo "El cálculo λ de homotopía es un sistema de tipos hipotético (en este momento)" y terminó con "En este momento, gran parte de lo que dije anteriormente está a nivel de conjeturas. Incluso la definición del modelo de TS en la categoría de homotopía no es trivial "refiriéndose a los complejos problemas de coherencia que no se resolvieron hasta 2009. Esta nota incluía una definición sintáctica de" tipos de igualdad "que se afirmaba que eran interpretados en el modelo por espacios de ruta, pero no consideraba Según las reglas de Martin-Löf para tipos de identidad. También estratificó los universos por dimensión de homotopía además del tamaño, una idea que luego fue descartada en su mayoría.

En el lado sintáctico, Benno van den Berg conjeturó en 2006 que la torre de tipos de identidad de un tipo en la teoría de tipos intensional debería tener la estructura de una categoría ω, y de hecho un grupo ω, en el sentido "globular, algebraico". de Michael Batanin. Esto fue posteriormente probado de forma independiente por van den Berg y Garner en el artículo "Los tipos son omega-groupoides débiles" (publicado en 2008), y por Peter Lumsdaine en el artículo "Categorías ω débiles de la teoría de tipos intensivos" (publicado en 2009) y como parte de su Ph.D. de 2010. tesis "Categorías superiores de las teorías de tipos".

El axioma de univalencia, la teoría de la homotopía sintética y los tipos inductivos superiores

El concepto de fibración univalente fue introducido por Voevodsky a principios de 2006. 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 de identidad, en el contexto vacío, pueden contener solo reflexividad, Voevodsky hizo No reconozco hasta 2009 que estos tipos de identidad pueden usarse en combinación con los universos univalentes. En particular, la idea de que la univalencia se puede introducir simplemente agregando un axioma a la teoría de tipos existente de Martin-Löf apareció solo en 2009.

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 utilizarse para resolver los problemas de coherencia de los modelos categóricos de la teoría de tipos. También demostró, utilizando 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 de caminos-espacio de la base.

Para formular la univalencia como un axioma, Voevodsky encontró una manera de definir "equivalencias" sintácticamente que tenía la propiedad importante de que el tipo que representa la declaración "f es una equivalencia" era (bajo el supuesto de extensionalidad de la función) (-1) -truncado (es decir, contráctil si está habitada). Esto le permitió dar una declaració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 la homotopía sintética" en el asistente de pruebas Coq ; esto formó la base de la biblioteca más tarde llamada "Fundaciones" y, finalmente, "UniMath".

La unificación de los diversos 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 código Coq a un grupo que incluía a Awodey, Warren, Lumsdaine y Robert Harper , Dan Licata, Michael Shulman , y otros. Esta reunión produjo los esbozos de una prueba (de Warren, Lumsdaine, Licata y Shulman) de que toda 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 funcional.

El siguiente evento fundamental fue un mini-taller 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 homotopía de la teoría de tipos constructivos". Como parte de un tutorial de Coq para este taller, Andrej Bauer escribió una pequeña biblioteca de Coq basada en las ideas de Voevodsky (pero sin usar ninguno de sus códigos); esto finalmente se convirtió en el núcleo de la primera versión de la biblioteca Coq "HoTT" (la primera confirmación de la última 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 tipos inductivos superiores, debido 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), si el axioma de univalencia tiene modelos no estándar (ya que Shulman respondió positivamente) y cómo para definir tipos (semi) simpliciales (todavía abiertos en MLTT, aunque se puede hacer en el Homotopy Type System (HTS) de Voevodsky, una teoría de tipos con dos tipos de igualdad).

Poco después del taller de Oberwolfach, se estableció el sitio web y el blog de Homotopy Type Theory , y el tema comenzó a popularizarse con ese nombre. Se puede obtener una idea de algunos de los avances importantes durante este período en el historial del blog.

Fundaciones univalentes

Todos están de acuerdo en que la frase "fundamentos univalentes" está estrechamente relacionada con la teoría de tipos de homotopía, pero no todos la usan de la misma manera. Vladimir Voevodsky lo utilizó originalmente para referirse a su visión de un sistema fundamental para las matemáticas en el que los objetos básicos son tipos de homotopía, basados ​​en una teoría de tipos que satisface el axioma de univalencia y formalizados en un asistente de pruebas informáticas.

A medida que el trabajo de Voevodsky se integró con la comunidad de otros investigadores que trabajaban en la teoría de tipos de homotopía, "fundamentos univalentes" a veces se usaba indistintamente con "teoría de tipos de homotopía", y otras veces para referirse solo a su uso como un sistema fundacional (excluyendo, por ejemplo, , el estudio de la semántica modelo-categórica o metateoría computacional). Por ejemplo, el tema del año especial de la IAS se clasificó oficialmente como "fundaciones univalentes", aunque gran parte del trabajo realizado allí se centró en la semántica y la metateoría además de las fundaciones. El libro producido por los participantes en el programa 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 usos, ya que el libro solo analiza HoTT como una base matemática.

Año especial sobre fundamentos univalentes de las matemáticas

Reproducir medios

Una animación que muestra el desarrollo del libro HoTT en el repositorio de GitHub por parte de los participantes en el proyecto Univalent Foundations Special Year.

En 2012-13, los investigadores del Instituto de Estudios Avanzados celebraron "Un año especial sobre los fundamentos univalentes de las matemáticas". El año especial reunió a investigadores en topología , ciencias de la computación , 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 , quien fue 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 que es análogo al de los matemáticos comunes que hacen teoría de conjuntos. Después de los experimentos iniciales, quedó claro que esto no solo era posible sino muy beneficioso, y que un libro (el llamado Libro HoTT ) podía y debía escribirse. Muchos otros participantes del proyecto se unieron al esfuerzo con soporte técnico, redacción, corrección de pruebas y ofrecimiento de 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 bifurcar su propia versión del libro, y se puede comprar en forma impresa y descargar de forma gratuita.

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

Participantes oficiales en el año especial

ACM Computing Reviews enumeró el libro como una publicación notable de 2013 en la categoría "matemáticas de la computación".

Conceptos clave

Teoría de tipos intensivos	Teoría de la homotopía
tipos ${\ Displaystyle A}$	espacios ${\ Displaystyle A}$
condiciones ${\ Displaystyle a}$	puntos ${\ Displaystyle a}$
${\ Displaystyle a: A}$	${\ Displaystyle a \ in A}$
tipo dependiente ${\ Displaystyle x: A \ \ vdash \ B (x) \}$	fibración ${\ Displaystyle B \ to A}$
Tipo de identidad ${\ Displaystyle \ mathrm {Id} _ {A} (a, b)}$	espacio de camino
${\ Displaystyle p: \ mathrm {Id} _ {A} (a, b)}$	sendero ${\ Displaystyle p: a \ to b}$
${\ Displaystyle \ alpha: \ mathrm {Id} _ {\ mathrm {Id} _ {A} (a, b)} (p, q)}$	homotopía ${\ Displaystyle \ alpha: p \ Rightarrow q}$

"Proposiciones como tipos"

HoTT usa una versión modificada de la interpretación de las " proposiciones como tipos " de la teoría de tipos, según la cual los tipos también pueden representar proposiciones y los términos pueden entonces representar demostraciones. En HoTT, sin embargo, a diferencia de las "proposiciones como tipos" estándar, las "meras proposiciones" juegan un papel especial que, hablando en términos generales, son aquellos tipos que tienen como máximo un término, hasta la igualdad proposicional . Se parecen más a proposiciones lógicas convencionales que a tipos generales, en el sentido de que son irrelevantes para la prueba.

Igualdad

El concepto fundamental de la teoría de tipos de homotopía es el camino . En HoTT, el tipo es el tipo de todas las rutas 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 al 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 , correspondiente a la propiedad simétrica de igualdad. Dos caminos de tipo resp. se puede concatenar, formando una ruta de tipo ; esto corresponde a la propiedad transitiva de la igualdad. ${\ Displaystyle a = b}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle a}$${\ Displaystyle a = a}$${\ Displaystyle a = b}$${\ Displaystyle b = a}$${\ Displaystyle a = b}$${\ Displaystyle b = c}$${\ Displaystyle a = c}$

Lo más importante es que, dado un camino y una prueba de alguna propiedad , la prueba puede "transportarse" a lo largo del camino para producir una prueba de la propiedad . (Dicho de manera equivalente, un objeto de tipo puede convertirse en un objeto de tipo ). Esto corresponde a la propiedad de sustitución de igualdad . Aquí, una diferencia importante entre HoTT y la matemática clásica entra en acción. En la matemática clásica, una vez que la igualdad de los dos valores y se ha establecido, y se pueden usar indistintamente a partir de entonces, sin tener en cuenta ninguna distinción entre ellos. En la teoría de tipos de homotopía, sin embargo, puede haber múltiples caminos diferentes , y transportar un objeto a lo largo de dos caminos 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é camino se está utilizando. ${\ Displaystyle p: a = b}$${\ Displaystyle P (a)}$${\ Displaystyle p}$${\ Displaystyle P (b)}$${\ Displaystyle P (a)}$${\ Displaystyle P (b)}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle a}$${\ Displaystyle b}$${\ Displaystyle a = b}$

En general, una "proposición" puede tener múltiples pruebas diferentes. (Por ejemplo, el tipo de todos los números naturales, cuando se considera una proposición, tiene cada número natural como prueba). Incluso si una proposición tiene solo una prueba , el espacio de caminos puede no ser 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 ruta trivial . ${\ Displaystyle a}$${\ Displaystyle a = a}$

Tenga en cuenta que la gente escribe para , dejando así el tipo de implícito. No lo confunda con , denotando la función de identidad en . ${\ Displaystyle a = b}$${\ Displaystyle Id_ {A} (a, b)}$${\ Displaystyle A}$${\ Displaystyle a, b}$${\ Displaystyle id_ {A}: A \ to A}$${\ Displaystyle A}$

Equivalencia de tipo

Dos tipos y pertenecientes a algún universo se definen como equivalentes si existe una equivalencia entre ellos. Una equivalencia es una función ${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle U}$

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

que tiene tanto una inversa izquierda como una inversa derecha, en el sentido de que para adecuadamente elegidos y , los siguientes tipos están habitados: ${\ Displaystyle g}$${\ Displaystyle 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 una inversa izquierda y una inversa derecha", utilizando tipos de igualdad. Tenga en cuenta que las condiciones de invertibilidad anteriores son tipos de igualdad en los tipos de función y . Generalmente se asume el axioma de extensionalidad de la función, que asegura que estos son equivalentes a los siguientes tipos que expresan invertibilidad usando la igualdad en el dominio y codominio y : ${\ Displaystyle f}$${\ displaystyle A \ rightarrow A}$${\ displaystyle B \ rightarrow B}$${\ Displaystyle A}$${\ Displaystyle 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 , ${\ Displaystyle x: A}$${\ Displaystyle 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}$.

El axioma de la univalencia

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

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

que expresa que los tipos que son iguales son, en particular, también equivalentes. ${\ Displaystyle A, B}$

El axioma de univalencia establece que esta función es en sí misma una equivalencia. 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'".

Aplicaciones

Demostración del teorema

HoTT permite que las pruebas matemáticas se traduzcan a un lenguaje de programación de computadoras para los asistentes de pruebas de computadoras mucho más fácilmente que antes. Este enfoque ofrece la posibilidad de que las computadoras verifiquen pruebas difíciles.

Uno de los objetivos de las matemáticas es formular axiomas de los que prácticamente todos los teoremas matemáticos puedan derivarse y probarse sin ambigüedades. Las pruebas correctas en matemáticas deben seguir las reglas de la lógica. Deben ser derivables sin error de axiomas y enunciados ya probados.

HoTT agrega el axioma de univalencia, que relaciona la igualdad de las proposiciones lógico-matemáticas con la teoría de la homotopía. Una ecuación como "a = b" 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 significa que las dos formas que representan los valores de los símbolos son topológicamente equivalentes.

Estas relaciones de equivalencia topológica, según el director del Instituto de Estudios Teóricos de ETH Zürich , Giovanni Felder , se pueden formular mejor en la teoría de la homotopía porque es más completa: la teoría de la homotopía explica no solo por qué "a es igual a b", sino también cómo derivar esto. En teoría de conjuntos, esta información tendría que definirse adicionalmente, lo que dificulta la traducción de proposiciones matemáticas a lenguajes de programación.

Programación de computadoras

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.

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

Sin embargo, se cree que ciertos objetos, como los tipos semi-simpliciales, 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 de fibra, que respetan las trayectorias, y tipos sin fibra, que no lo hacen. 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.

Ver también

• Cálculo de construcciones
• Correspondencia Curry-Howard
• Teoría de tipos intuicionistas
• Hipótesis de homotopía
• Fundaciones univalentes

Referencias

Bibliografía

Otras lecturas

• David Corfield (2020), Teoría del tipo de homotopía modal: la perspectiva de una nueva lógica para la filosofía , Oxford University Press.

enlaces externos

• Teoría del tipo de homotopía
• Teoría de tipos de homotopía en nLab
• Wiki la teoría del tipo de homotopía
• Página web de Vladimir Voevodsky sobre las fundaciones univalentes
• 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" - Conferencia en video de Steve Awodey en el Instituto de Estudios Avanzados

Bibliotecas de matemáticas formalizadas