¿Cuál es la relación (y el estado) de los Fundamentos Univalentes y la Teoría de Tipos de Homotopía?

Question

Parece que UniMath y HoTT en GitHub están activos hasta el día de hoy. Las páginas de Wikipedia tienen ambos enlaces entre sí.

Sin estar empapado de ambas áreas, ¿cómo se relacionan y cuál es la situación de los dos proyectos? ¿Supera HoTT a UniMath, de manera que UniMath es una encarnación heredada/anterior de los fundamentos generales, y HoTT es el último desarrollo de la idea/hilo? ¿O compiten de alguna manera?

Answer 1

En primer lugar, permítanme señalar que el título de esta pregunta es engañoso: la diferencia entre Fundamentos univalentes y Teoría de los tipos de homotopía es una cuestión distinta de la diferencia entre UniMath y el Biblioteca HoTT . (Los primeros están bien descritos en sus artículos de Wikipedia, por lo que el lector interesado en esa cuestión puede ser remitido allí).

Tanto UniMath como la biblioteca HoTT son bibliotecas de matemáticas según un principio univalente en el lenguaje de (variaciones de) la teoría de tipos de homotopía. Aunque UniMath se originó en primer lugar, a partir de la obra de Voevodsky Biblioteca de fundaciones Ambos están todavía en desarrollo activo. La introducción de Bauer-Gross-Lumsdaine La biblioteca HoTT: Una formalización de la teoría de tipos de homotopía en Coq explica la diferencia de filosofía entre los dos proyectos (en la sección Consistencia ).

La diferencia esencial es que UniMath adopta la postura de desconfiar de Coq tanto como sea posible, utilizando sólo las características más básicas del lenguaje (por ejemplo, las presentes en la Teoría de Tipos de Martin-Löf), porque el sistema de tipos de Coq es, en algunos lugares, ad hoc, y no se ha demostrado que estas combinaciones de características sean realmente sólidas. Evitando las características avanzadas del lenguaje (no demostradas), UniMath espera evitar la posible inconsistencia derivada de un sistema de tipos poco sólido.

Por otro lado, la biblioteca HoTT se preocupa más por la formalización que es más fácil de usar, permitiendo así características avanzadas del lenguaje, a costa de introducir potencialmente la falta de solidez cuando se utilizan características no probadas de Coq:

Por esta razón [para evitar posibles inconsistencias], UniMath evita casi todas las características de Coq (incluso, por ejemplo, los tipos de registro), restringiéndose en la medida de lo posible restringiéndose en lo posible a la teoría de tipos estándar de Martin-Löf (excepto para asumir Type : Type en todo momento, para simular el de Voevodsky). Sin embargo, esta restricción no puede ser aplicada por el núcleo. Creemos más bien que los asistentes de pruebas y la formalización informática de las matemáticas están en una fase tan temprana que vale la pena experimentar, aun a riesgo de introducir una incoherencia de introducir una incoherencia (que es bastante leve, debido a las cuentas semánticas conocidas de los fragmentos de la teoría).

Desde un punto de vista pragmático, dado que las bibliotecas se han desarrollado en paralelo, también hay diferencias en las características que ambas bibliotecas soportan actualmente (como la gama de definiciones matemáticas y teoremas).