Teoría del tipo de homotopía

Teoría de tipos en lógica y matemáticas.

Portada de la teoría de tipos 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 ) 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 este tipo de teorías de tipos; el uso de la teoría de tipos como lógica (o lenguaje interno ) para la teoría de la 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 (que incluye 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 informáticos .

Existe una gran superposición entre el trabajo denominado 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 en el punto de vista y el énfasis. ^[1] 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 cambia rápidamente.

Historia

modelo grupoide

Hubo un tiempo en que la idea de que los tipos en la teoría de tipos intensional con sus tipos de identidad podían considerarse grupoides era folklore 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 teoría de tipos, aunque sólo "unidimensional " (los modelos tradicionales en la categoría de conjuntos son homotópicamente de dimensión 0).

Su artículo de seguimiento ^[3] presagió varios desarrollos posteriores en la teoría de tipos de homotopía. Por ejemplo, observaron que el modelo grupoide satisface una regla que llamaron "extensionalidad universal", que no es otra que la restricción a tipos 1 del axioma de univalencia que Vladimir Voevodsky propuso diez años después. (Sin embargo, el axioma para los tipos 1 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 utiliza grupoides de dimensiones superiores, para tales categorías se tendría que "la equivalencia es igualdad"; Esto lo demostraron más tarde Benedikt Ahrens, Krzysztof Kapulkin y Michael Shulman . ^[4]

Historia temprana: categorías de modelos y grupoides superiores.

Los primeros modelos de dimensiones superiores 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 ^[5] en la que Warren dio una charla titulada "Modelos de homotopía de la teoría de tipos intensional", que también sirvió como prospecto de su tesis (el comité de tesis presente fueron Awodey, Nicola Gambino y Alex Simpson). En el resumen del prospecto de tesis de Warren se incluye un resumen. ^[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 intencionales". Ideas relacionadas fueron discutidas en las charlas por Steve Awodey, "Teoría de tipos de categorías de dimensiones superiores", y Thomas Streicher , "Tipos de identidad versus grupos 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 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 presentado en 2009 por Voevodsky, otro en 2010 por van den Berg y Garner. ^[9] Lumsdaine y Warren finalmente dieron una solución general, basada en la construcción de Voevodsky, en 2014. ^[10]

En el PSSL86 en 2007 ^[11] Awodey dio una charla titulada "Teoría del tipo 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 se publicó 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.

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 de Tipos "Una nota muy breve sobre el cálculo lambda de homotopía ", ^[14] que esbozaba las líneas generales de una teoría de tipos con productos, sumas y universos dependientes y de un modelo de esta teoría de tipos en Kan simplicial. conjuntos . Comenzó diciendo "El cálculo de homotopía λ es un sistema de tipo hipotético (por el momento)" y terminó con "Por el momento, mucho de lo que dije anteriormente está al nivel de conjeturas. Incluso la definición del modelo de TS en la categoría de homotopía no es trivial", en referencia a las complejas cuestiones 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 camino, pero que no consideraban 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 parte.

Desde el punto de vista 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 grupoide ω, en el sentido "globular, algebraico". de Miguel Batanin. Esto fue demostrado más tarde de forma independiente por van den Berg y Garner en el artículo "Los tipos son grupos omega débiles" (publicado en 2008), ^[15] y por Peter Lumsdaine en el artículo "Categorías ω débiles de la teoría de tipos intensional" (publicado en 2009). ) y como parte de su doctorado de 2010. tesis "Categorías superiores de las teorías de tipos". ^[dieciséis]

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. ^[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 de identidad, en el contexto vacío, pueden contener sólo reflexividad Voevodsky no reconoció hasta 2009 que estos tipos de identidad pueden usarse en combinación con los universos univalentes. En particular, la idea de que la univalencia puede introducirse simplemente añadiendo un axioma a la teoría de tipos existente de Martin-Löf apareció recién en 2009. ^{[a] [b]}

También en 2009, Voevodsky resolvió 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ó, 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 importante propiedad de que el tipo que representa la declaración "f es una equivalencia" estaba (bajo el supuesto de extensionalidad de la función) (-1) truncado (es decir contraíble si está habitada). Esto le permitió dar una declaración sintáctica de univalencia, generalizando la "extensionalidad universal" 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 la homotopía sintética" en el asistente de prueba Coq ; esto formó la base de la biblioteca que más tarde se llamó "Foundations" y, finalmente, "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 las líneas generales 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 para equivalencias adjuntas. Poco después, Voevodsky demostró que el axioma de univalencia implica extensionalidad de la función.

El siguiente evento fundamental 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 de la homotopía 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 Coq ^[21] basada en las ideas de Voevodsky (pero sin usar nada de su código); esto eventualmente se convirtió en el núcleo de la primera versión de la biblioteca 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 tipos inductivos superiores, debida 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 (ya que respondieron positivamente por Shulman), 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 el blog Homotopy Type Theory ^[26] , 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 la historia del blog. ^[27]

Cimentaciones univalentes

Todos coinciden 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, basado en una teoría de tipos que satisface § el axioma de univalencia y formalizado en un asistente de prueba por computadora. ^[28]

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 usaban indistintamente con "teoría de tipos de homotopía", ^[29] y otras veces para referirse sólo a su uso como sistema fundamental (excluyendo , por ejemplo, el estudio de la semántica categórica de modelos o la metateoría computacional). ^[30] Por ejemplo, el tema del año especial de la 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 elaborado por los participantes del 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 sólo analiza HoTT como base matemática. ^[29]

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

Una animación que muestra el desarrollo del Libro HoTT en el repositorio de GitHub por parte de los participantes en el proyecto del Año Especial de Univalent Foundations.

En 2012-2013, investigadores del Instituto de Estudios Avanzados celebraron "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 comunes que hacen teoría de conjuntos. Después de los primeros experimentos quedó claro que esto no sólo era posible sino también muy beneficioso, y que se podía y debía escribir un libro (el llamado Libro HoTT ) ^{[29] [32]} . Muchos otros participantes del proyecto se unieron al esfuerzo brindando soporte técnico, redacción, corrección de pruebas y ofreciendo ideas. Inusualmente para un texto de matemáticas, se desarrolló en colaboración y de forma 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. ^{[33] [34] [35]}

En términos más generales, 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 en el año especial.

• Peter Aczel
• Benedikt Ahrens
• Thorsten Altenkirch
• Steve Awodey
• Bruno Barras
• Andrej Bauer
• Yves Bertot
• Marc Bezem
• Thierry Coquand
• Eric Finster
• Daniel Grayson
• Hugo Herbelín
• Andre Joyal
• Dan Licata
• Peter Lumsdaine
• Assia Mahboubi
• Por Martin-Löf
• Serguéi Mélijov
• Álvaro Pelayo
• Andres Polonsky
• Michael Shulman
• Matthieu Sozeau
• Escupidores bajos
• Benno van den Berg
• Vladímir Voevodski
• Michael Warren
• Noam Zeilberger

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

Conceptos clave

"Proposiciones como tipos"

HoTT utiliza una versión modificada de la interpretación de " 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 representar pruebas. Sin embargo, en HoTT, a diferencia de las "proposiciones como tipos" estándar, desempeñan un papel especial las "simples proposiciones", que en términos generales son aquellos tipos que tienen como máximo un término, hasta la igualdad proposicional . Éstas 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 un punto a otro . (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 , correspondiente a la propiedad reflexiva de igualdad. Una ruta de tipo se puede invertir, formando una ruta 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, dada una ruta y una prueba de alguna propiedad , la prueba se puede "transportar" a lo largo de la ruta para producir una prueba de la propiedad . (Dicho de manera equivalente, un objeto de tipo se puede convertir 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 establecida la igualdad de dos valores , y puede 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 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 sólo 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 contenga sólo 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 implícito . No lo confunda con , que denota la función de identidad en . ^[C] ${\displaystyle a=b}$ ${\displaystyle Id_{A}(a,b)}$ ${\displaystyle A}$ ${\displaystyle a,b}$ ${\displaystyle id_{A}:A\to A}$ ${\displaystyle A}$

Equivalencia de tipos

Dos tipos y pertenecientes a algún universo se definen como equivalentes si existe 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 elegidos adecuadamente 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 éstas 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 de tipo.

${\displaystyle A\to B}$

junto con una prueba de que son equivalencias se denotan por

${\displaystyle A\simeq B}$.

El axioma de univalencia

Habiendo definido funciones que son equivalencias como arriba, 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),}$

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. ^{[29] : 115  [18] : 4–6} Por lo tanto, tenemos

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

"En otras palabras, identidad es equivalente a 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]}

Aplicaciones

demostración de teoremas

Los defensores afirman que HoTT permite que las pruebas matemáticas se traduzcan a un lenguaje de programación informática para los asistentes de pruebas informáticas mucho más fácilmente que antes. Argumentan que este enfoque aumenta el potencial de las computadoras para verificar pruebas difíciles. ^[37] Sin embargo, estas afirmaciones no son universalmente aceptadas y muchos esfuerzos de investigación y asistentes de prueba no utilizan 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 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. ^[37] ${\displaystyle a=b}$

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

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. ^[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 semisimpliciales, 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 los caminos, y tipos no fibrantes, que no. La teoría de tipos computacional cúbica cartesiana es la primera teoría de tipos de dos niveles que ofrece una interpretación computacional completa de la teoría de tipos de homotopía. ^[40]

Ver también

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

Notas

1. La univalencia es un tipo, una propiedad del tipo de identidad IdU de un universo U —Martín Hötzel Escardó (2018) ^{[18] : p.1}
2. "La univalencia es un tipo, y el axioma de univalencia dice que este tipo tiene algún habitante". ^{[18] : pág.1}
3. Aquí se utiliza la convención de la teoría de tipos, según la cual los nombres de los tipos comienzan con una letra mayúscula, pero los nombres de las funciones comienzan con una letra minúscula.
4. Martín Hötzel Escardó ha demostrado que la propiedad de univalencia, "una propiedad del tipo de identidad IdU de un universo U", ^{[18] : 4} puede tener o no un habitante. Según el axioma de univalencia, el tipo 'isUnivalent(U)' tiene un habitante; Hötzel Escardó señala que cuando la reflexión es la única manera de construir elementos del tipo de identidad, distintos de la univalencia, se puede construir una función J a partir del tipo de identidad, de la reflexión y de J. ^{[18] : 2.4 El tipo de identidad} Hötzel Escardó procede a construir el tipo de univalencia, utilizando aplicaciones repetidas de J. Cuando 'todos los tipos son conjuntos' (denominado Axioma K), ^{[18] : 2.4} El axioma K implica que el tipo 'esUnivalente(U)' no tiene un habitante. Así, Hötzel Escardó encuentra que el tipo 'isUnivalent(U)' está indeciso en la teoría de tipos de Martin-Löf (MLTT). ^{[18] : 3.2, p.6 El axioma de univalencia}

Referencias

1. Shulman, Michael (27 de enero de 2016). "Teoría del tipo de homotopía: un enfoque sintético para igualdades superiores". arXiv : 1601.05035v3 [math.LO]., nota al pie 1
2. Hofmann, M.; Streicher, T. (1994). "El modelo grupoide refuta la unicidad de las pruebas de identidad". Actas del Noveno Simposio Anual del IEEE sobre Lógica en Ciencias de la Computación . págs. 208-212. doi :10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID  19496198.
3. Hofmann, Martín; Streicher, Thomas (1998). "La interpretación grupoide de la teoría de tipos". En Sambin, Giovanni; Smith, Jan M. (eds.). Veinticinco años de teoría de tipos constructivos . Guías de lógica de Oxford. vol. 36. Prensa de Clarendon. págs. 83-111. ISBN 978-0-19-158903-4. SEÑOR  1686862.
4. Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael (2015). "Categorías univalentes y finalización de Rezk". Estructuras matemáticas en informática . 25 (5): 1010–1039. arXiv : 1303.0584 . doi :10.1017/S0960129514000486. SEÑOR  3340533. S2CID  1135785.
5. "Métodos fundamentales en informática 2006, Universidad de Calgary, 7 al 9 de junio de 2006". Universidad de Calgary . Consultado el 6 de junio de 2021 .
6. Warren, Michael A. (2006). Modelos de homotopía de la teoría de tipos intensionales (PDF) (Tesis).
7. "Tipos de identidad: estructura topológica y categórica, taller, Uppsala, 13 y 14 de noviembre de 2006". Universidad de Uppsala - Departamento de Matemáticas . Consultado el 6 de junio de 2021 .
8. Richard Garner, Axiomas de factorización para la teoría de tipos
9. Berg, Benno van den; Garner, Richard (27 de julio de 2010). "Modelos topológicos y simplificados de tipos de identidad". arXiv : 1007.4638 [matemáticas.LO].
10. Lumsdaine, Peter LeFanu; Warren, Michael A. (6 de noviembre de 2014). "El modelo de universos locales: una construcción de coherencia pasada por alto para teorías de tipo dependiente". Transacciones ACM sobre lógica computacional . 16 (3): 1–31. arXiv : 1411.1736 . doi :10.1145/2754931. S2CID  14068103.
11. "86ª edición del Seminario peripatético sobre gavillas y lógica, Universidad Henri Poincaré, 8 y 9 de septiembre de 2007". loria.fr. Archivado desde el original el 17 de diciembre de 2014 . Consultado el 20 de diciembre de 2014 .
12. Lista preliminar de participantes de PSSL86
13. Awodey, Steve; Warren, Michael A. (3 de septiembre de 2007). "Modelos teóricos de homotopía de tipos de identidad". Actas matemáticas de la Sociedad Filosófica de Cambridge . 146 (1): 45. arXiv : 0709.0248 . Código Bib : 2008MPCPS.146...45A. doi :10.1017/S0305004108001783. S2CID  7915709.
14. Voevodsky, Vladimir (27 de septiembre de 2006). "Una nota muy breve sobre el cálculo λ de homotopía". ucr.edu . Consultado el 6 de junio de 2021 .
15. van den Berg, Benno; Garner, Richard (1 de diciembre de 2007). "Los tipos son grupos omega débiles". Actas de la Sociedad Matemática de Londres . 102 (2): 370–394. arXiv : 0812.0298 . doi :10.1112/plms/pdq026. S2CID  5575780.
16. Lumsdaine, Peter (2010). "Categorías superiores de las teorías de tipos" (PDF) (Ph.D.). Universidad de Carnegie mellon.
17. Notas sobre el cálculo lambda de homotopía, marzo de 2006
18. Martín Hötzel Escardó (18 de octubre de 2018) Una formulación autónoma, breve y completa del axioma de univalencia de Voevodsky
19. Repositorio de GitHub, Matemáticas Univalentes
20. Awodey, Steve; Garner, Richard; Martin-Löf, Per; Voevodsky, Vladimir (27 de febrero - 5 de marzo de 2011). "Minitaller: La interpretación de la homotopía de la teoría de tipos constructivos" (PDF) . Informes Oberwolfach . Instituto de Investigaciones Matemáticas de Oberwolfach: 609–638. doi : 10.4171/OWR/2011/11 . Consultado el 6 de junio de 2021 .
21. Repositorio de GitHub, Andrej Bauer, Teoría de la homotopía en Coq
22. Bauer, Andrej; Voevodsky, Vladimir (29 de abril de 2011). "Teoría básica de tipos de homotopía". GitHub . Consultado el 6 de junio de 2021 .
23. Repositorio de GitHub, teoría del tipo de homotopía
24. Shulman, Michael (2015). "Univalencia para diagramas inversos y canonicidad de homotopía". Estructuras matemáticas en informática . 25 (5): 1203-1277. arXiv : 1203.3253 . doi :10.1017/S0960129514000565. S2CID  13595170.
25. Licata, Daniel R.; Harper, Robert (21 de julio de 2011). "Canonicidad para la teoría de tipos bidimensionales" (PDF) . Universidad de Carnegie mellon . Consultado el 6 de junio de 2021 .
26. Blog sobre teoría de tipos de homotopía y fundamentos univalentes
27. Blog de teoría de tipos de homotopía
28. Teoría de tipos y fundamentos univalentes
29. Programa de Fundaciones Univalentes abcde (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas. Instituto de Estudios Avanzados.
30. Teoría del tipo de homotopía: referencias
31. Escuela de matemáticas IAS: año especial sobre los fundamentos univalentes de las matemáticas
32. Anuncio oficial de The HoTT Book, por Steve Awodey, 20 de junio de 2013
33. Monroe, D (2014). "¿Un nuevo tipo de matemáticas?". Comunicaciones ACM . 57 (2): 13-15. doi :10.1145/2557446. S2CID  6120947.
34. Shulman, Mike (20 de junio de 2013). "El libro HoTT". El Café de categoría n . Consultado el 6 de junio de 2021 a través de la Universidad de Texas.
35. Bauer, Andrej (20 de junio de 2013). "El libro HoTT". Matemáticas y Computación . Consultado el 6 de junio de 2021 .
36. Reseñas de informática ACM . "El mejor de 2013".
37. Meyer, Florian (3 de septiembre de 2014). "Una nueva base para las matemáticas". Revista I+D . Consultado el 29 de julio de 2021 .
38. Sojakova, Kristina (2015). Tipos inductivos superiores como álgebras homotópicas iniciales. POPL 2015. arXiv : 1402.0761 . doi :10.1145/2676726.2676983.
39. Cohen, Cirilo; Coquand, Thierry; Huber, Simón; Mörtberg, Anders (2015). Teoría de tipos cúbicos: una interpretación constructiva del axioma de univalencia. TIPOS 2015.
40. Anguili, Carlo; Favonia; Harper, Robert (2018). Teoría de tipos computacionales cúbicos cartesianos: razonamiento constructivo con caminos e igualdades (PDF) . Lógica Informática 2018 . Consultado el 26 de agosto de 2018 .(a aparecer)

Bibliografía

• El Programa de Fundaciones Univalentes (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas. Princeton, Nueva Jersey: Instituto de Estudios Avanzados . SEÑOR  3204653.(Versión de GitHub citada en este artículo).
• Awodey, S .; Warren, MA (enero de 2009). "Modelos teóricos de homotopía de tipos de identidad". Actas matemáticas de la Sociedad Filosófica de Cambridge . 146 (1): 45–55. arXiv : 0709.0248 . Código Bib : 2008MPCPS.146...45A. doi :10.1017/S0305004108001783. S2CID  7915709.Como PDF.
• Awodey, Steve (2012). "Teoría de tipos y homotopía" (PDF) . En Dybjer, P.; Lindström, Sten; Palmgren, Erik; et al. (eds.). Epistemología versus Ontología . Lógica, epistemología y unidad de la ciencia. Saltador. págs. 183-201. CiteSeerX  10.1.1.750.3626 . doi :10.1007/978-94-007-4435-6_9. ISBN 978-94-007-4434-9. S2CID  4499538.
• Awodey, Steve (2014). "Estructuralismo, invariancia y univalencia". Filosofía Matemática . 22 (1): 1–11. CiteSeerX  10.1.1.691.8113 . doi :10.1093/philmat/nkt030.
• Hofmann, Martín; Streicher, Thomas (1998). "La interpretación grupoide de la teoría de tipos". En Sambin, G.; Smith, JM (eds.). Veinticinco años de teoría de tipos constructivos . Prensa de Clarendon. págs. 83-112. ISBN 978-0-19-158903-4.Como posdata.
• Rijke, Egbert (2012). Teoría de tipos de homotopía (PDF) (Maestría). Universidad de Utrecht.
• Voevodsky, Vladimir (2006), Una nota muy breve sobre el cálculo de homotopía Lambda (PDF)
• Voevodsky, Vladimir (2010), El axioma de equivalencia y los modelos univalentes de la teoría de tipos , arXiv : 1402.5556 , Bibcode :2014arXiv1402.5556V
• Warren, Michael A. (2008). Aspectos teóricos de la homotopía de la teoría de tipos constructivos (PDF) (Ph.D.). Universidad de Carnegie mellon.

Otras lecturas

• 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.

enlaces externos

• Teoría del tipo de homotopía
• Teoría del tipo de homotopía en el n Lab
• Wiki de teoría de tipos de homotopía
• Página web de Vladimir Voevodsky sobre las Fundaciones Univalentes
• Teoría de tipos de homotopía y 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

Bibliotecas de matemáticas formalizadas.

• Biblioteca de fundaciones (2010-actualidad)
• Biblioteca HoTT (2011-actualidad), 30 de enero de 2022
• Biblioteca P-adics (2011-2012)
• Biblioteca RezkCompletion, enero de 2022(ahora integrado en UniMath, donde se lleva a cabo un mayor desarrollo)
• Biblioteca de teoría
• Biblioteca UniMath (2014-actualidad), 25 de enero de 2022