Fundamentos univalentes

Los fundamentos univalentes son un enfoque de los fundamentos de las matemáticas en el que las estructuras matemáticas se construyen a partir de objetos llamados tipos . En los fundamentos univalentes, los tipos no se corresponden exactamente con nada en los fundamentos de la teoría de conjuntos , pero pueden concebirse como espacios, donde los tipos iguales corresponden a espacios homotópicamente equivalentes y los elementos iguales de un tipo corresponden 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 se apartan del uso de la lógica de predicados clásica como sistema de deducción formal subyacente (aunque también son compatibles con ella) , reemplazándola, por el momento, con una versión de la teoría de tipos de Martin-Löf . El desarrollo de los fundamentos univalentes está estrechamente relacionado con el desarrollo de la teoría de tipos homotópicos .

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 entre 2006 y 2009. La única referencia sobre 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 homotópicos ( 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 demostración modernos como Rocq (anteriormente conocido como Coq ) y Agda . La primera biblioteca de este tipo, llamada "Foundations", fue creada por Vladimir Voevodsky en 2010. ^{[ 5 ]} Ahora Foundations forma parte de un desarrollo más amplio con varios autores llamado UniMath . ^{[ 6 ]} Foundations también inspiró 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 charla de Thierry Coquand en el Seminario Bourbaki ^{[ 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 denomina " lógica de primer orden con tipos dependientes" (FOLDS). ^{[ 10 ]} La principal distinción entre los fundamentos univalentes y los fundamentos concebidos por Makkai es el reconocimiento de que los "análogos de conjuntos de dimensiones superiores" corresponden a grupoides infinitos y que las categorías deben considerarse como análogos de conjuntos parcialmente ordenados de dimensiones superiores .

Originalmente, Vladimir Voevodsky ideó los fundamentos univalentes con el objetivo de permitir que quienes trabajan en matemáticas puras clásicas utilizaran computadoras para verificar sus teoremas y construcciones. El hecho de que los fundamentos univalentes sean inherentemente constructivos se descubrió durante el proceso de escritura de la biblioteca Foundations (ahora parte de UniMath). Actualmente, en los 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 el principio del tercero excluido como supuesto, y un "cociente" de las matemáticas constructivas por la relación de equivalencia módulo el axioma del tercero excluido.

En el sistema de formalización para fundaciones univalentes que se basa en la teoría de tipos de Martin-Löf y sus derivados, como el Cálculo de Construcciones Inductivas , los análogos de conjuntos de dimensiones superiores se representan mediante tipos. La colección de tipos se estratifica según 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 contraíbles.

Los tipos de nivel h 1 son aquellos en los que cualesquiera dos elementos son iguales. Dichos 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 ]} Así pues, 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 fundamentos univalentes se denomina 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 solo si X es contraíble. Es un teorema (que se denomina, en la biblioteca UniMath, isapropiscontr ) que para cualquier X el tipo iscontr X tiene nivel h 1 y, por lo tanto, ser un tipo contraíble es una propiedad. Esta distinción entre las propiedades que se observan en objetos de tipo h-nivel 1 y las estructuras que se observan en objetos de tipos h-niveles superiores es muy importante en los fundamentos univalentes.

Los tipos de nivel h 2 se denominan conjuntos. ^{[ 11 ]} Es un teorema que el tipo de los números naturales tiene nivel h 2 ( isasetnat en UniMath). Los creadores de las fundaciones 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 teoría de conjuntos, tanto constructivas como clásicas. ^{[ 13 ]}

Las categorías se definen (véase la biblioteca RezkCompletion en UniMath) como tipos de nivel h 3 con una estructura adicional muy similar a la estructura de los tipos de nivel h 2 que define conjuntos parcialmente ordenados. La teoría de categorías en fundamentos univalentes es algo diferente y más rica que la teoría de categorías en el mundo de la teoría de conjuntos, siendo la distinción clave la que existe entre precategorías y categorías. ^{[ 14 ]}

Una explicación de las ideas principales de los fundamentos univalentes y su conexión con las matemáticas constructivas se puede encontrar en un tutorial de Thierry Coquand. ^{[ a ]} ​​Una presentación de las ideas principales desde la perspectiva de las matemáticas clásicas se puede encontrar en la reseña de 2014 de Álvaro Pelayo y Michael Warren, ^{[ 17 ]} así como en la introducción ^{[ 18 ]} de Daniel Grayson. Véase también: Vladimir Voevodsky (2014). ^{[ 19 ]}

Una descripción 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 se puede encontrar en un artículo de Chris Kapulkin, Peter LeFanu Lumsdaine y Vladimir Voevodsky. ^{[ 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 tercero excluido para proposiciones.

El modelo de Voevodsky se considera no constructivo, ya que utiliza el axioma de elección de una manera ineliminable.

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. Una solución parcial se esboza en un artículo de Marc Bezem , Thierry Coquand y Simon Huber ^{[ 23 ]} , siendo la cuestión clave pendiente la propiedad computacional del eliminador para los tipos identidad. Las ideas de este artículo se están desarrollando actualmente en varias direcciones, incluyendo 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 los fundamentos univalentes se está realizando utilizando varios subsistemas y extensiones del Cálculo de Construcciones Inductivas (CCI).

Existen tres problemas estándar cuya solución, a pesar de muchos intentos, no pudo construirse utilizando CIC:

1. Para definir los tipos de tipos semisimpliciales, tipos H o estructuras de categoría (infty,1) en tipos.
2. Ampliar CIC con un sistema de gestión de universos que permita la implementación de las reglas de redimensionamiento.
3. Para desarrollar una variante constructiva del Axioma de Univalencia ^{[ 25 ]}

Estos problemas sin resolver indican que, si bien CIC es un buen sistema para la fase inicial del desarrollo de los fundamentos univalentes, avanzar hacia el uso de asistentes de demostración computacionales en el trabajo sobre sus aspectos más sofisticados requerirá el desarrollo de una nueva generación de sistemas formales de deducción y computación.

• teoría de tipos homotópicos

• Definición de univalente en el diccionario Wikcionario

Bibliotecas de matemáticas formalizadas

• Biblioteca de fundamentos (2010-actualidad)
• Biblioteca HoTT (2011-actualidad) , 27 de enero de 2022
• Introducción a los fundamentos univalentes de las matemáticas con Agda