Teoría del tipo de homotopía

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

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

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 corresponde a veces a diferencias en el punto de vista y el énfasis. ^[1] Como tal, 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 flujo.

Historia

Prehistoria: el modelo grupoide

En un tiempo, la idea de que los tipos en la teoría de tipos intensionales 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 . ^[2] 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 . ^[3]

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 ^[4] en la que Warren dio una charla titulada "Modelos de homotopía de la teoría de tipo intensional", que también sirvió como prospecto de su 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. ^[5]

En un taller posterior sobre tipos de identidad en la Universidad de Uppsala en 2006 ^[6] 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", ^[7] y otra de Michael. Warren, "Categorías modelo 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. ^[8] Lumsdaine y Warren finalmente dieron una solución general, basada en la construcción de Voevodsky, en 2014. ^[9]

En el PSSL86 en 2007 ^[10] 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 ^[11] ). 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 ^[12] 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 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 ", ^[13] 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 Kan simplicial. conjuntos . 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), ^[14] 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. tesis "Categorías superiores de las teorías de tipos". ^[15]

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. ^[16] 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 no reconoció hasta 2009 que estos tipos de identidad se pueden usar 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 las "equivalencias" sintácticamente que tenía la propiedad importante de que el tipo que representaba 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 fue capaz de 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 "Fundaciones" y, finalmente, "UniMath". ^[17]

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". ^[18] Como parte de un tutorial de Coq para este taller, Andrej Bauer escribió una pequeña biblioteca de Coq ^[19] basada en las ideas de Voevodsky (pero sin utilizar ninguno de sus códigos); esto finalmente se convirtió en el núcleo de la primera versión de la biblioteca Coq "HoTT" ^[20] (la primera confirmación de la última ^[21] 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 ^[22]^[23] ), si el axioma de univalencia tiene modelos no estándar (ya que se respondió positivamente por Shulman), y cómo definir tipos (semi) simpliciales (todavía 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 estableció el sitio web y el blog de Homotopy Type Theory ^[24] , 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. ^[25]

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

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", ^[27] y otras veces para referirse solo a su uso como un sistema fundacional (excluyendo , por ejemplo, el estudio de la semántica categórica del modelo o la metateoría computacional). ^[28] Por ejemplo, el tema del año especial de la IAS se clasificó 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 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. ^[27]

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". ^[29] 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 ) ^[27]^[30] 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 forma 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. ^[31]^[32]^[33]

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

Peter Aczel
Benedikt Ahrens
Thorsten Altenkirch
Steve Awodey
Bruno Barras
Andrej Bauer
Yves Bertot
Marc Bezem
Thierry Coquand
Eric Finster
Daniel Grayson
Hugo Herbelin
André Joyal
Dan Licata
Peter Lumsdaine
Assia Mahboubi
Por Martin-Löf
Sergey Melikhov
Álvaro Pelayo
Andrew Polonsky
Michael Shulman
Matthieu Sozeau
Bas Spitters
Benno van den Berg
Vladimir Voevodsky
Michael Warren
Noam Zeilberger

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

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)}$	camino ${\ 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 ${\ Displaystyle a = b}$ es el tipo de todos los caminos desde el punto ${\ Displaystyle a}$ al punto ${\ Displaystyle b}$ . (Por lo tanto, una prueba de que un punto ${\ Displaystyle a}$ es igual a un punto ${\ Displaystyle b}$ es lo mismo que un camino desde el punto ${\ Displaystyle a}$ al punto ${\ Displaystyle b}$ .) Para cualquier punto ${\ Displaystyle a}$ , existe una ruta de tipo ${\ Displaystyle a = a}$ , correspondiente a la propiedad reflexiva de la igualdad. Un camino de tipo ${\ Displaystyle a = b}$ se puede invertir, formando un camino de tipo ${\ Displaystyle b = a}$ , correspondiente a la propiedad simétrica de igualdad. Dos caminos de tipo ${\ Displaystyle a = b}$ resp. ${\ Displaystyle b = c}$ se puede concatenar, formando una ruta de tipo ${\ Displaystyle a = c}$ ; esto corresponde a la propiedad transitiva de la igualdad.

Lo más importante, dado un camino ${\ Displaystyle p: a = b}$ , y una prueba de alguna propiedad ${\ Displaystyle P (a)}$ , la prueba se puede "transportar" a lo largo del camino ${\ Displaystyle p}$ para presentar una prueba de la propiedad ${\ Displaystyle P (b)}$ . (Dicho de manera equivalente, un objeto de tipo ${\ Displaystyle P (a)}$ se puede convertir en un objeto de tipo ${\ Displaystyle P (b)}$ .) Corresponde a la propiedad de sustitución de la 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 la igualdad de dos valores ${\ Displaystyle a}$ y ${\ Displaystyle b}$ Ha sido establecido, ${\ Displaystyle a}$ y ${\ Displaystyle b}$ pueden usarse 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 ${\ Displaystyle a = b}$ , y el transporte de un objeto por 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.

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 cada número natural como prueba). 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 esté vacío o que contenga solo un punto con un espacio de ruta trivial .

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

Equivalencia de tipo

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

{\ Displaystyle f: A \ to B}

que tiene una inversa izquierda y una inversa derecha, en el sentido de que para adecuadamente elegido ${\ Displaystyle g}$ y ${\ Displaystyle h}$ , los siguientes tipos están habitados:

{\ 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 " ${\ Displaystyle f}$ 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 ${\ displaystyle A \ rightarrow A}$ y ${\ displaystyle B \ rightarrow B}$ . 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 ${\ Displaystyle A}$ y ${\ 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 ${\ Displaystyle x: A}$ y ${\ 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 ese tipo ${\ 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. ^[27]^{: 115} 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'". ^[27]^{: 4}

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

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

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

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

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

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

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

Ver también

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

Referencias

^ Shulman, Michael (27 de enero de 2016). "Teoría del tipo de homotopía: un enfoque sintético para mayores igualdades". arXiv : 1601.05035v3 [ math.LO ]., nota al pie 1
^ Hofmann, Martin; 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 constructiva de tipos . Guías lógicas de Oxford. 36 . Prensa de Clarendon. págs. 83-111. ISBN 978-0-19-158903-4. Señor 1686862 .
^ Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael (2015). "Categorías univalentes y la terminación Rezk". Estructuras matemáticas en informática . 25 (5): 1010–1039. arXiv : 1303.0584 . doi : 10.1017 / S0960129514000486 . Señor 3340533 . S2CID 1135785 .
^ "Métodos Fundamentales en Ciencias de la Computación 2006, Universidad de Calgary, 7 al 9 de junio de 2006" . Universidad de Calgary . Consultado el 6 de junio de 2021 .
^ Warren, Michael A. (2006). Modelos de homotopía de la teoría de tipos intensivos (PDF) (Tesis).
^ "Tipos de identidad - estructura topológica y categórica, taller, Uppsala, 13-14 de noviembre de 2006" . Universidad de Uppsala - Departamento de Matemáticas . Consultado el 6 de junio de 2021 .
^ Richard Garner, axiomas de factorización para la teoría de tipos
^ Berg, Benno van den; Garner, Richard (27 de julio de 2010). "Modelos topológicos y simpliciales de tipos de identidad". arXiv : 1007.4638 [ matemáticas.LO ].
^ 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 las teorías de tipo dependiente". Transacciones ACM en lógica computacional . 16 (3): 1–31. arXiv : 1411,1736 . doi : 10.1145 / 2754931 . S2CID 14068103 .
^ "86ª edición del Seminario Peripatético de Gavillas y Lógica, Universidad Henri Poincaré, 8-9 de septiembre de 2007" . loria.fr.^{[ enlace muerto ]}
^ Lista preliminar de participantes de PSSL86
^ Awodey, Steve; Warren, Michael A. (3 de septiembre de 2007). "Modelos teóricos de homotopía de tipos de identidad". Procedimientos matemáticos de la Sociedad Filosófica de Cambridge . 146 : 45. arXiv : 0709.0248 . Código Bibliográfico : 2008MPCPS.146 ... 45A . doi : 10.1017 / S0305004108001783 . S2CID 7915709 .
^ Voevodsky, Vladimir (27 de septiembre de 2006). "Una nota muy breve sobre homotopía λ-cálculo" . ucr.edu . Consultado el 6 de junio de 2021 .
^ van den Berg, Benno; Garner, Richard (1 de diciembre de 2007). "Los tipos son omega-grupoides débiles". Actas de la London Mathematical Society . 102 (2): 370–394. arXiv : 0812.0298 . doi : 10.1112 / plms / pdq026 . S2CID 5575780 .
^ Lumsdaine, Peter (2010). "Categorías superiores de las teorías de tipos" (PDF) (Ph.D.). Universidad de Carnegie mellon.
^ Notas sobre el cálculo de homotopía lambda, marzo de 2006
^ Repositorio de GitHub, Matemáticas univalentes
^ "Mini-taller: la interpretación de la homotopía de la teoría constructiva de tipos" (PDF) . Instituto de Investigaciones Matemáticas de Oberwolfach. 27 de febrero a 5 de marzo de 2011. doi : 10.4171 / OWR / 2011/11 . Consultado el 6 de junio de 2021 .
^ Repositorio de GitHub, Andrej Bauer, Teoría de homotopía en Coq
^ Bauer, Andrej; Voevodsky, Vladimir (29 de abril de 2011). "Teoría básica del tipo de homotopía" . GitHub . Consultado el 6 de junio de 2021 .
^ Repositorio de GitHub, teoría del tipo de homotopía
^ 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 .
^ Licata, Daniel R .; Harper, Robert (21 de julio de 2011). "Canonicidad para la teoría de tipos bidimensionales" (PDF) . Universidad Carnegie Mellon . Consultado el 6 de junio de 2021 .
^ Blog de teoría de tipos de homotopía y fundaciones univalentes
^ Blog de teoría de tipos de homotopía
^ Teoría de tipos y fundamentos univalentes
^ a b c d e Programa de Fundaciones Univalentes (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas . Instituto de Estudios Avanzados.
^ Teoría del tipo de homotopía: referencias
^ Escuela de matemáticas IAS: año especial sobre los fundamentos univalentes de las matemáticas
^ Anuncio oficial de The HoTT Book, por Steve Awodey, 20 de junio de 2013
^ Monroe, D (2014). "¿Un nuevo tipo de matemáticas?" . Comm ACM . 57 (2): 13-15. doi : 10.1145 / 2557446 . S2CID 6120947 .
^ Shulman, Mike (20 de junio de 2013). "El libro de HoTT" . El Café de categoría n . Consultado el 6 de junio de 2021 , a través de la Universidad de Texas.
^ Bauer, Andrej (20 de junio de 2013). "El libro de HoTT" . Matemáticas y Computación . Consultado el 6 de junio de 2021 .
^ Reseñas de computación ACM . "Lo mejor de 2013" .
^ a b c d Meyer, Florian (3 de septiembre de 2014). "Una nueva base para las matemáticas" . R & D Magazine . Consultado el 6 de septiembre de 2014 .
^ Sojakova, Kristina (2015). Tipos inductivos superiores como álgebras iniciales de homotopía . POPL 2015. arXiv : 1402.0761 . doi : 10.1145 / 2676726.2676983 .
^ Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). Teoría de tipos cúbicos: una interpretación constructiva del axioma de univalencia . TIPOS 2015.
^ Anguili, Carlo; Favonia; Harper, Robert (2018). Teoría del tipo computacional cúbico cartesiano: razonamiento constructivo con caminos e igualdad (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". Procedimientos matemáticos de la Sociedad Filosófica de Cambridge . 146 (1): 45–55. arXiv : 0709.0248 . Código Bibliográfico : 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". Philosophia Mathematica . 22 (1): 1–11. CiteSeerX 10.1.1.691.8113 . doi : 10.1093 / philmat / nkt030 .
Hofmann, Martin; 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 constructiva de tipos . 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), The Equivalence Axiom and Univalent Models of Type Theory , arXiv : 1402.5556 , Bibcode : 2014arXiv1402.5556V
Warren, Michael A. (2008). Aspectos teóricos de la homotopía de la teoría constructiva de tipos (PDF) (Ph.D.). Universidad de Carnegie mellon.

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

Biblioteca de fundaciones (2010-actual)
Biblioteca HoTT (2011-actual)
Biblioteca P-adics (2011-2012)
Biblioteca RezkCompletion (ahora integrado en UniMath, donde se lleva a cabo un mayor desarrollo)
Biblioteca de Ktheory
Biblioteca UniMath (2014-actual)

[1] Shulman, Michael (27 de enero de 2016). "Teoría del tipo de homotopía: un enfoque sintético para mayores igualdades". arXiv : 1601.05035v3 [ math.LO ]., nota al pie 1

[2] Hofmann, Martin; 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 constructiva de tipos . Guías lógicas de Oxford. 36 . Prensa de Clarendon. págs. 83-111. ISBN 978-0-19-158903-4. Señor 1686862 .

[3] Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael (2015). "Categorías univalentes y la terminación Rezk". Estructuras matemáticas en informática . 25 (5): 1010–1039. arXiv : 1303.0584 . doi : 10.1017 / S0960129514000486 . Señor 3340533 . S2CID 1135785 .

[4] "Métodos Fundamentales en Ciencias de la Computación 2006, Universidad de Calgary, 7 al 9 de junio de 2006" . Universidad de Calgary . Consultado el 6 de junio de 2021 .

[5] Warren, Michael A. (2006). Modelos de homotopía de la teoría de tipos intensivos (PDF) (Tesis).

[6] "Tipos de identidad - estructura topológica y categórica, taller, Uppsala, 13-14 de noviembre de 2006" . Universidad de Uppsala - Departamento de Matemáticas . Consultado el 6 de junio de 2021 .

[7] Richard Garner, axiomas de factorización para la teoría de tipos

[8] Berg, Benno van den; Garner, Richard (27 de julio de 2010). "Modelos topológicos y simpliciales de tipos de identidad". arXiv : 1007.4638 [ matemáticas.LO ].

[9] 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 las teorías de tipo dependiente". Transacciones ACM en lógica computacional . 16 (3): 1–31. arXiv : 1411,1736 . doi : 10.1145 / 2754931 . S2CID 14068103 .

[10] "86ª edición del Seminario Peripatético de Gavillas y Lógica, Universidad Henri Poincaré, 8-9 de septiembre de 2007" . loria.fr.^{[ enlace muerto ]}

[11] Lista preliminar de participantes de PSSL86

[12] Awodey, Steve; Warren, Michael A. (3 de septiembre de 2007). "Modelos teóricos de homotopía de tipos de identidad". Procedimientos matemáticos de la Sociedad Filosófica de Cambridge . 146 : 45. arXiv : 0709.0248 . Código Bibliográfico : 2008MPCPS.146 ... 45A . doi : 10.1017 / S0305004108001783 . S2CID 7915709 .

[13] Voevodsky, Vladimir (27 de septiembre de 2006). "Una nota muy breve sobre homotopía λ-cálculo" . ucr.edu . Consultado el 6 de junio de 2021 .

[14] van den Berg, Benno; Garner, Richard (1 de diciembre de 2007). "Los tipos son omega-grupoides débiles". Actas de la London Mathematical Society . 102 (2): 370–394. arXiv : 0812.0298 . doi : 10.1112 / plms / pdq026 . S2CID 5575780 .

[15] Lumsdaine, Peter (2010). "Categorías superiores de las teorías de tipos" (PDF) (Ph.D.). Universidad de Carnegie mellon.

[16] Notas sobre el cálculo de homotopía lambda, marzo de 2006

[UniMath-17] Repositorio de GitHub, Matemáticas univalentes

[18] "Mini-taller: la interpretación de la homotopía de la teoría constructiva de tipos" (PDF) . Instituto de Investigaciones Matemáticas de Oberwolfach. 27 de febrero a 5 de marzo de 2011. doi : 10.4171 / OWR / 2011/11 . Consultado el 6 de junio de 2021 .

[19] Repositorio de GitHub, Andrej Bauer, Teoría de homotopía en Coq

[20] Bauer, Andrej; Voevodsky, Vladimir (29 de abril de 2011). "Teoría básica del tipo de homotopía" . GitHub . Consultado el 6 de junio de 2021 .

[21] Repositorio de GitHub, teoría del tipo de homotopía

[22] 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 .

[23] Licata, Daniel R .; Harper, Robert (21 de julio de 2011). "Canonicidad para la teoría de tipos bidimensionales" (PDF) . Universidad Carnegie Mellon . Consultado el 6 de junio de 2021 .

[24] Blog de teoría de tipos de homotopía y fundaciones univalentes

[25] Blog de teoría de tipos de homotopía

[26] Teoría de tipos y fundamentos univalentes

[hott-27] Programa de Fundaciones Univalentes (2013). Teoría de tipos de homotopía: fundamentos univalentes de las matemáticas . Instituto de Estudios Avanzados.

[28] Teoría del tipo de homotopía: referencias

[29] Escuela de matemáticas IAS: año especial sobre los fundamentos univalentes de las matemáticas

[30] Anuncio oficial de The HoTT Book, por Steve Awodey, 20 de junio de 2013

[31] Monroe, D (2014). "¿Un nuevo tipo de matemáticas?" . Comm ACM . 57 (2): 13-15. doi : 10.1145 / 2557446 . S2CID 6120947 .

[32] Shulman, Mike (20 de junio de 2013). "El libro de HoTT" . El Café de categoría n . Consultado el 6 de junio de 2021 , a través de la Universidad de Texas.

[33] Bauer, Andrej (20 de junio de 2013). "El libro de HoTT" . Matemáticas y Computación . Consultado el 6 de junio de 2021 .

[34] Reseñas de computación ACM . "Lo mejor de 2013" .

[:0-35] Meyer, Florian (3 de septiembre de 2014). "Una nueva base para las matemáticas" . R & D Magazine . Consultado el 6 de septiembre de 2014 .

[36] Sojakova, Kristina (2015). Tipos inductivos superiores como álgebras iniciales de homotopía . POPL 2015. arXiv : 1402.0761 . doi : 10.1145 / 2676726.2676983 .

[37] Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). Teoría de tipos cúbicos: una interpretación constructiva del axioma de univalencia . TIPOS 2015.

[38] Anguili, Carlo; Favonia; Harper, Robert (2018). Teoría del tipo computacional cúbico cartesiano: razonamiento constructivo con caminos e igualdad (PDF) . Lógica informática 2018 . Consultado el 26 de agosto de 2018 . (a aparecer)

[1]