teoría de tipos homotópicos

En un principio, la idea de que los tipos en la teoría de tipos intensional con sus tipos identidad podían considerarse grupoides era un mito matemático . Se hizo precisa semánticamente por primera vez en el artículo de 1994 de Martin Hofmann y Thomas Streicher titulado "El modelo de grupoide refuta la unicidad de las pruebas de identidad" ^{[ 2 ]} , 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 solo "unidimensional " (los modelos tradicionales en la categoría de conjuntos son homotópicamente cero-dimensionales).

Su artículo posterior ^{[ 3 ]} anticipó varios desarrollos posteriores en la teoría de tipos homotópicos. Por ejemplo, observaron que el modelo de grupoide satisface una regla que denominaron "extensionalidad del universo", que no es otra cosa que la restricción a 1-tipos del axioma de univalencia que Vladimir Voevodsky propuso 10 años después. (Sin embargo, el axioma para 1-tipos es notablemente más sencillo 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 utilizara grupoides de dimensiones superiores, para tales categorías se tendría "equivalencia es igualdad"; esto fue demostrado posteriormente 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 categorías de modelos de Quillen . Estos resultados se presentaron públicamente por primera vez en la conferencia FMCS 2006 ^{[ 5 ]} , donde Warren dio una charla titulada "Modelos de homotopía de la teoría de tipos intensionales", que también sirvió como propuesta de tesis (el comité de tesis presente estaba compuesto por Awodey, Nicola Gambino y Alex Simpson). Un resumen se encuentra en el resumen de la propuesta 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 intensional 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 modelo y tipos de identidad intensional". 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 omega-categorías débiles" donde esbozó 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 tuvieron que lidiar con el problema de coherencia típico de los modelos de la teoría de tipos dependientes, y se desarrollaron varias soluciones. Una de ellas fue presentada en 2009 por Voevodsky, y otra en 2010 por van den Berg y Garner. ^{[ 9 ]} Una solución general, basada en la construcción de Voevodsky, fue finalmente presentada por Lumsdaine y Warren en 2014. ^{[ 10 ]}

En el PSSL86 de 2007 ^{[ 11 ],} Awodey dio una charla titulada "Teoría de tipos homotópicos" (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 de teoría homotópica de tipos identidad", que se publicó en el servidor de preimpresiones ArXiv en 2007 ^{[ 13 ]} y se publicó en 2009; una versión más detallada apareció en la tesis de Warren "Aspectos de teoría homotópica de la teoría constructiva de tipos" en 2008.

Casi al mismo tiempo, Vladimir Voevodsky investigaba 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 homotópico " ^{[ 14 ]} , que esbozaba los contornos 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 de Kan . Comenzaba diciendo "El cálculo λ homotópico es un sistema de tipos hipotético (por el momento)" y terminaba con "Por el momento, gran parte de lo que he dicho anteriormente está al nivel de conjeturas. Incluso la definición del modelo de TS en la categoría homotópica 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, según se afirmaba, se interpretaban en el modelo mediante espacios de caminos, pero no consideraba las reglas de Per Martin-Löf para los tipos identidad. Además del tamaño, también estratificaba los universos según la dimensión de homotopía, una idea que posteriormente fue descartada en gran medida.

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 intensional debería tener la estructura de una ω-categoría, y de hecho un ω-grupoide, en el sentido "globular y 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". ^{[ 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 profundizó en los detalles de un modelo de teoría de tipos en complejos de Kan y observó que la existencia de una fibración universal de Kan podía utilizarse para resolver los problemas de coherencia de los modelos categóricos de teoría de tipos. Asimismo, demostró, basándose en una idea de A. K. 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 axioma, Voevodsky encontró una manera de definir sintácticamente las "equivalencias" que poseía la importante propiedad de que el tipo que representaba la afirmación "f es una equivalencia" estaba (bajo el supuesto de extensionalidad de la función) truncado (-1) (es decir, contraíble si estaba habitado). Esto le permitió dar una formulación sintáctica de la univalencia, generalizando la "extensionalidad del universo" de Hofmann y Streicher a dimensiones superiores. También pudo utilizar 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 Rocq (anteriormente conocido como Coq ); esto formó la base de la biblioteca que más tarde se denominó "Foundations" y finalmente "UniMath". ^{[ 19 ]}

La unificación de los distintos hilos de investigación comenzó en febrero de 2010 con una reunión informal en la Universidad Carnegie Mellon , donde Voevodsky presentó su modelo en complejos de Kan y su versión de Rocq a un grupo que incluía a Awodey, Warren, Lumsdaine, Robert Harper , Dan Licata, Michael Shulman y otros. Esta reunión produjo los esbozos de una demostración (por Warren, Lumsdaine, Licata y Shulman) de que toda equivalencia homotópica 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 la extensionalidad de la función.

El siguiente evento clave 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 homotópica de la teoría de tipos constructiva". ^{[ 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 finalmente se convirtió en el núcleo de la primera versión de la biblioteca "HoTT" de Coq ^{[ 22 ]} (el primer commit 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 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 abierto, aunque algunos casos especiales se han resuelto positivamente ^{[ 24 ] [ 25 ]} ), si el axioma de univalencia tiene modelos no estándar (ya que Shulman respondió positivamente) y cómo definir tipos (semi)simpliciales (aún abierto 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 blog de la Teoría de Tipos Homotópicos ^{[ 26 ]} , y el tema comenzó a popularizarse bajo ese nombre. Una idea de algunos de los avances importantes durante este período puede obtenerse del historial del blog. ^{[ 27 ]}

HoTT utiliza una versión modificada de la interpretación de la teoría de tipos que considera las proposiciones como tipos , según la cual los tipos también pueden representar proposiciones y los términos, a su vez, pueden representar pruebas. Sin embargo, en HoTT, a diferencia de la interpretación estándar de las proposiciones como tipos, las "meras proposiciones" desempeñan un papel especial. En términos generales, se trata de tipos que tienen como máximo un término, salvo igualdad proposicional . Estas se asemejan más a las proposiciones lógicas convencionales que a los tipos generales, ya que son irrelevantes para las pruebas.

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

Lo más importante es que se nos ha dado un camino.${\displaystyle p:a=b}$y una prueba de alguna propiedad${\displaystyle P(a)}$, la prueba puede ser "transportada" a lo largo del camino${\displaystyle p}$para producir una prueba de la propiedad${\displaystyle P(b)}$. (Dicho de forma equivalente, un objeto de tipo${\displaystyle P(a)}$puede convertirse en un objeto de tipo${\displaystyle P(b)}$.) Esto corresponde a la propiedad de sustitución de la igualdad . Aquí, surge una diferencia importante entre HoTT y las matemáticas clásicas. En matemáticas clásicas, una vez que la igualdad de dos valores${\displaystyle a}$y${\displaystyle b}$se ha establecido,${\displaystyle a}$y${\displaystyle b}$Pueden usarse indistintamente a partir de entonces, sin tener en cuenta ninguna distinción entre ellos. Sin embargo, en la teoría de tipos homotópicos, puede haber múltiples caminos diferentes.${\displaystyle a=b}$y transportar un objeto por dos caminos diferentes dará como resultado dos resultados distintos. Por lo tanto, en la teoría de tipos homotópicos, al aplicar la propiedad de sustitución, es necesario especificar qué camino se está utilizando.

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

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

Dos funciones${\displaystyle f,g:A\rightarrow B}$son homotopías por identificación puntual: ^{[ 29 ] : 2.4.1}

${\displaystyle f\sim g:\equiv \prod _{x:A}f(x)=g(x)}$

Equivalencias entre dos tipos${\displaystyle A}$y${\displaystyle B}$perteneciente a algún universo${\displaystyle U}$se definen mediante las funciones${\displaystyle f:A\rightarrow B}$junto con la prueba de tener retracciones y secciones con respecto a homotopías: ^{[ 29 ] : 2.4.11,2.4.10}

${\displaystyle A\simeq B:\equiv \sum _{f:A\rightarrow B}{\text{isequiv}}(f)}$, dónde

${\displaystyle {\text{isequiv}}(f):\equiv \left(\sum _{g:B\rightarrow A}(f\circ g)\sim id_{B}\right)\times \left(\sum _{h:B\rightarrow A}(h\circ f)\sim id_{A}\right)}$

Junto con el axioma de univalencia que se presenta a continuación, se obtiene un " no circular"${\displaystyle \infty }$-isomorfismo" se extendió a identidad. ^{[ 37 ]}

${\displaystyle A\simeq B:\equiv {\text{hay}}\ f:A\leftrightarrows B:g\ {\text{con}}\ g\circ f\simeq id_{A}\ {\text{y}}\ f\circ g\simeq id_{B}}$

Habiendo definido funciones que son equivalencias como se indicó anteriormente, 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 cual expresa que los tipos${\displaystyle A,B}$que son iguales son, en particular, también equivalentes.

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\imeq 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 ]} Esto se debe a que la equivalencia de tipos es compatible con todas las construcciones de la teoría de tipos ^{[ 29 ] : 2.6-2.15} .

Los defensores afirman que HoTT permite traducir demostraciones matemáticas a un lenguaje de programación para asistentes de demostración computacionales con mucha más facilidad que antes. Argumentan que este enfoque aumenta el potencial de las computadoras para verificar demostraciones complejas. ^{[ 38 ]} Sin embargo, estas afirmaciones no son universalmente aceptadas y muchos proyectos de investigación y asistentes de demostración no se basan en HoTT.

HoTT adopta el axioma de univalencia, que relaciona la igualdad de proposiciones lógico-matemáticas con la teoría de la homotopía. Una ecuación como${\displaystyle 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 homotópicos, esto significa que las dos formas que representan los valores de los símbolos son topológicamente equivalentes. ^{[ 38 ]}

Giovanni Felder, director del Instituto de Estudios Teóricos de la ETH Zúrich, sostiene que 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 explica no solo 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 sus defensores, dificulta la traducción de proposiciones matemáticas a lenguajes de programación. ^{[ 38 ]}

A partir de 2015, se estaba llevando a cabo un intenso trabajo de investigación para modelar y analizar formalmente el comportamiento computacional del axioma de univalencia en la teoría de tipos homotópicos. ^{[ 39 ]}

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

Sin embargo, se cree que ciertos objetos, como los tipos semisimpliciales, no pueden construirse sin hacer referencia a alguna noción de igualdad exacta. Por lo tanto, se han desarrollado diversas teorías de tipos de dos niveles que dividen sus tipos en tipos fibrantes, que respetan las trayectorias, y tipos no fibrantes, que no lo hacen. La teoría de tipos computacional cúbica cartesiana es la primera teoría de tipos de dos niveles que proporciona una interpretación computacional completa a la teoría de tipos homotópicos. ^{[ 40 ]}