Los fundamentos univalentes son una aproximación a los fundamentos de las matemáticas en la que las estructuras matemáticas se construyen a partir de objetos llamados tipos . Los tipos en fundamentos univalentes no corresponden exactamente a nada en fundamentos de teoría de conjuntos , pero pueden considerarse como espacios, con tipos iguales correspondientes a espacios equivalentes de homotopía y con elementos iguales de un tipo correspondientes a puntos de un espacio conectados por un camino. . Los fundamentos univalentes se inspiran tanto en las antiguas ideas platónicas de Hermann Grassmann y Georg Cantor como en las matemáticas " categóricas " al estilo de Alexander Grothendieck . Los fundamentos univalentes parten del uso de la lógica de predicados clásica como sistema de deducción formal subyacente (aunque también son compatibles con él) , reemplazándola, de momento, por una versión de la teoría de tipos de Martin-Löf . El desarrollo de fundamentos univalentes está estrechamente relacionado con el desarrollo de la teoría de tipos de homotopía .
Los fundamentos univalentes son compatibles con el estructuralismo , si se adopta una noción apropiada (es decir, categórica) de estructura matemática. [1]
Las ideas principales de los fundamentos univalentes fueron formuladas por Vladimir Voevodsky durante los años 2006 a 2009. La única referencia para las conexiones filosóficas entre los fundamentos univalentes y las ideas anteriores son las conferencias Bernays de Voevodsky de 2014. [2] El nombre "univalencia" se debe a Voevodsky. [3] [4] Una discusión más detallada de la historia de algunas de las ideas que contribuyen al estado actual de los fundamentos univalentes se puede encontrar en la página sobre teoría de tipos de homotopía ( HoTT ).
Una característica fundamental de los fundamentos univalentes es que, cuando se combinan con la teoría de tipos de Martin-Löf ( MLTT ), proporcionan un sistema práctico para la formalización de las matemáticas modernas. Una cantidad considerable de matemáticas se ha formalizado utilizando este sistema y asistentes de prueba modernos como Coq y Agda . La primera biblioteca de este tipo llamada "Foundations" fue creada por Vladimir Voevodsky en 2010. [5] Ahora Foundations es parte de un desarrollo más amplio con varios autores llamado UniMath. [6] Las fundaciones también inspiraron otras bibliotecas de matemáticas formalizadas, como la biblioteca HoTT Coq [7] y la biblioteca HoTT Agda, [8] que desarrollaron ideas univalentes en nuevas direcciones.
Un hito importante para las fundaciones univalentes fue la conferencia del Seminario Bourbaki impartida por Thierry Coquand [9] en junio de 2014.
Los fundamentos univalentes se originaron a partir de ciertos intentos de crear fundamentos de las matemáticas basados en la teoría de categorías superiores . Las ideas anteriores más cercanas a los fundamentos univalentes fueron las ideas que Michael Makkai denota " lógica de primer orden con tipos dependientes" (FOLDS). [10] La principal distinción entre fundamentos univalentes y los fundamentos previstos por Makkai es el reconocimiento de que "análogos de conjuntos de dimensiones superiores" corresponden a grupoides infinitos y que las categorías deben considerarse como análogos de dimensiones superiores de conjuntos parcialmente ordenados .
Originalmente, Vladimir Voevodsky ideó los fundamentos univalentes con el objetivo de permitir a quienes trabajan en matemáticas puras clásicas utilizar computadoras para verificar sus teoremas y construcciones. El hecho de que los fundamentos univalentes son inherentemente constructivos se descubrió en el proceso de redacción de la biblioteca Foundations (ahora parte de UniMath). En la actualidad, en fundamentos univalentes, las matemáticas clásicas se consideran una "retracción" de las matemáticas constructivas , es decir, las matemáticas clásicas son a la vez un subconjunto de las matemáticas constructivas que consiste en aquellos teoremas y construcciones que utilizan la ley del tercero excluido como su supuesto y un "cociente" de matemáticas constructivas por la relación de ser equivalente módulo el axioma del tercero excluido.
En el sistema de formalización para fundamentos univalentes que se basa en la teoría de tipos de Martin-Löf y sus descendientes, como el Cálculo de construcciones inductivas , los análogos de conjuntos de dimensiones superiores están representados por tipos. La colección de tipos está estratificada por el concepto de nivel h (o nivel de homotopía ). [11]
Los tipos de nivel h 0 son aquellos iguales al tipo de un punto. También se les llama tipos contráctiles.
Los tipos de nivel h 1 son aquellos en los que dos elementos cualesquiera son iguales. Estos tipos se denominan "proposiciones" en fundamentos univalentes. [11] La definición de proposiciones en términos del nivel h concuerda con la definición sugerida anteriormente por Awodey y Bauer. [12] Entonces, si bien todas las proposiciones son tipos, no todos los tipos son proposiciones. Ser una proposición es una propiedad de un tipo que requiere prueba. Por ejemplo, la primera construcción fundamental en cimentaciones univalentes se llama iscontr . Es una función de tipos a tipos. Si X es un tipo, entonces iscontr X es un tipo que tiene un objeto si y sólo si X es contraíble. Es un teorema (que se llama, en la biblioteca UniMath, isapropiscontr ) que para cualquier X el tipo iscontr X tiene h-nivel 1 y, por lo tanto, ser un tipo contráctil es una propiedad. Esta distinción entre propiedades atestiguadas por objetos de tipos de nivel h 1 y estructuras atestiguadas por objetos de tipos de niveles h superiores es muy importante en los cimientos univalentes.
Los tipos de nivel h 2 se denominan conjuntos. [11] Es un teorema que el tipo de números naturales tiene h-nivel 2 ( isasetnat en UniMath). Los creadores de fundamentos univalentes afirman que la formalización univalente de conjuntos en la teoría de tipos de Martin-Löf es el mejor entorno disponible actualmente para el razonamiento formal sobre todos los aspectos de las matemáticas de la teoría de conjuntos, tanto constructivas como clásicas. [13]
Las categorías se definen (consulte la biblioteca RezkCompletion en UniMath) como tipos de h-nivel 3 con una estructura adicional que es muy similar a la estructura de los tipos de h-nivel 2 que define conjuntos parcialmente ordenados. La teoría de las categorías en fundamentos univalentes es algo diferente y más rica que la teoría de las categorías en el mundo de la teoría de conjuntos, siendo la nueva distinción clave la que existe entre precategorías y categorías. [14]
En un tutorial de Thierry Coquand se puede encontrar una descripción de las ideas principales de los fundamentos univalentes y su conexión con las matemáticas constructivas. [a] Se puede encontrar una presentación de las ideas principales desde la perspectiva de las matemáticas clásicas en la revisión de 2014 de Alvaro Pelayo y Michael Warren, [17] así como en la introducción [18] de Daniel Grayson. Véase también: Vladimir Voevodsky (2014). [19]
En un artículo de Chris Kapulkin, Peter LeFanu Lumsdaine y Vladimir Voevodsky se puede encontrar un relato de la construcción de Voevodsky de un modelo univalente de la teoría de tipos de Martin-Löf con valores en conjuntos simpliciales de Kan. [20] Michael Shulman construyó modelos univalentes con valores en las categorías de diagramas inversos de conjuntos simpliciales . [21] Estos modelos han demostrado que el axioma de univalencia es independiente del axioma del medio excluido para las proposiciones.
El modelo de Voevodsky se considera no constructivo ya que utiliza el axioma de elección de forma no eliminable.
El problema de encontrar una interpretación constructiva de las reglas de la teoría de tipos de Martin-Löf que además satisfaga el axioma de univalencia [b] y la canonicidad para los números naturales sigue abierto. En un artículo de Marc Bezem, Thierry Coquand y Simon Huber [23] se describe una solución parcial, siendo la cuestión clave la propiedad computacional del eliminador de los tipos de identidad. Las ideas de este artículo se están desarrollando ahora en varias direcciones, incluido el desarrollo de la teoría de tipos cúbicos. [24]
La mayor parte del trabajo sobre la formalización de las matemáticas en el marco de fundamentos univalentes se realiza utilizando varios subsistemas y extensiones del Cálculo de Construcciones Inductivas (CIC).
Hay tres problemas estándar cuya solución, a pesar de muchos intentos, no se pudo construir usando CIC:
Estos problemas no resueltos indican que si bien el CIC es un buen sistema para la fase inicial del desarrollo de los fundamentos univalentes, avanzar hacia el uso de asistentes de prueba informáticos en el trabajo sobre sus aspectos más sofisticados requerirá el desarrollo de una nueva generación de sistemas de deducción formales. y sistemas de computación.
La definición del diccionario de univalente en Wikcionario