The internal languages of univalent categories

Resumen Técnico: Los Lenguajes Internos de las Categorías Univalentes

Planteamiento del Problema
Los teoremas de lenguajes internos en la lógica categórica establecen una equivalencia entre la sintaxis (teorías de tipos) y la semántica (modelos categóricos). Un resultado seminal de Clairambault y Dybjer [CD14] corrigió el teorema original de Seely [See84], estableciendo una biequivalencia entre la bicatégora de las categorías localmente cartesianas cerradas (LCCC) y la bicatégora de las categorías democráticas con familias (CwF) que admiten tipos de identidad extensionales, tipos $\Sigma$ y tipos $\Pi$.

Sin embargo, este resultado fue formulado dentro de los fundamentos de la teoría de conjuntos. En los fundamentos univalentes (Teoría de Tipos Homotópica), la noción estándar de CwF encuentra un obstáculo fundamental: el axioma de univalencia implica que el tipo de los conjuntos no es un conjunto en sí mismo (es un 1-tipo). En consecuencia, el requisito en las CwF de que la colección de tipos en un contexto forme un conjunto es violado por la categoría univalente de conjuntos. Además, la distinción entre la estructura "elegida" (por ejemplo, fibraciones partidas o split fibrations) y la estructura "existente" (por ejemplo, límites hasta isomorfismo) crea problemas de coherencia en los fundamentos de la teoría de conjuntos que requieren el axioma de elección o procedimientos de estricteza (strictification). En los fundamentos univalentes, donde el isomorfismo implica identidad, estas distinciones se evaporan, pero el marco existente de las CwF no es directamente aplicable.

Metodología
El artículo desarrolla un nuevo marco para la semántica categórica dentro de los fundamentos univalentes, utilizando categorías univalentes y categorías de comprensión en lugar de CwF.

1. Categorías Univalentes: El autor trabaja con categorías donde el tipo de identidad de los objetos es equivalente al tipo de los isomorfismos (equivalencias adjuntas). Esto permite tratar las equivalencias adjuntas como identidades, simplificando las pruebas sobre la preservación de la estructura (por ejemplo, exponenciales) y eliminando la necesidad del axioma de elección para seleccionar límites.
2. Categorías de Comprensión: Para modelar tipos dependientes sin requerir que los tipos formen un conjunto, el artículo adopta categorías de comprensión (basadas en fibraciones y categorías desplegadas). Una categoría de comprensión consiste en una categoría base de contextos, una categoría desplegada de tipos, un desdoblamiento (cleaving, que proporciona sustitución) y un functor de comprensión. El autor restringe su atención a categorías de comprensión completas univalentes, donde tanto la base como la categoría desplegada son univalentes.
3. Bicatégoras Desplegadas: La construcción de las bicatégoras de modelos se basa fuertemente en las bicatégoras desplegadas [AFM+21]. Este enfoque modular permite al autor construir bicatégoras complejas (como las de LCCC o toposes con universos) mediante la superposición de propiedades (por ejemplo, límites finitos, tipos $\Pi$, universos) sobre bicatégoras base más simples. Esta modularidad facilita la prueba de que las bicatégoras resultantes son, ellas mismas, univalentes.
4. Propiedades Locales: Para extender los resultados de las categorías con límites finitos a estructuras más complejas como los toposes, el artículo adapta la noción de propiedades locales de Maietti [Mai05]. Una propiedad local es una condición sobre categorías cerradas bajo el proceso de corte (slicing). El autor formaliza esto dentro del marco de las bicatégoras desplegadas para extender las biequivalencias desde el caso base (límites finitos) hacia diversas clases de toposes.
5. Reindexación y Universos: Para el tratamiento de los universos, el artículo emplea la reindexación de bicatégoras desplegadas. Esta técnica permite la transferencia de una biequivalencia de una categoría base a una categoría desplegada sobre ella, permitiendo la definición de universos cerrados bajo formadores de tipos específicos (por ejemplo, $\Sigma$, $\Pi$, números naturales), sin requerir leyes de estabilidad estrictas, sino más bien estabilidad hasta isomorfismo (que se convierte en identidad en las categorías univalentes).

Contribuciones Clave
El artículo realiza cuatro contribuciones primarias:

1. Análogo Univalente de Clairambault-Dybjer: El autor construye una biequivalencia entre la bicatégora de categorías univalentes con límites finitos y la bicatégora de categorías de comprensión democráticas de límite finito (DFL) completas y univalentes. Esto establece que el lenguaje interno de las categorías univalentes con límites finitos es la teoría de tipos de Martin-Löf extensional con unidad, producto binario y tipos $\Sigma$.
2. Extensión a Categorías Localmente Cartesianas Cerradas: La biequivalencia se extiende a las categorías univalentes localmente cartesianas cerradas y a las categorías de comprensión DFL que admiten tipos $\Pi$. Esto confirma que el lenguaje interno de las LCCC univalentes es la teoría de tipos de Martin-Löf extensional con tipos $\Pi$.
3. Extensión a Toposes y Universos: El método se generaliza a varias clases de toposes (pretoposes, $\Pi$-pretoposes, toposes elementales y toposes con un objeto de números naturales) utilizando propiedades locales. Además, el autor define universos en estas categorías que están cerrados bajo formadores de tipos (números naturales, clasificador de subobjetos, reducción de proposiciones, tipos $\Sigma$ y tipos $\Pi$), estableciendo una biequivalencia para los toposes elementales con un universo.
4. Formalización: Todas las construcciones y pruebas se formalizan en el asistente de pruebas Rocq utilizando la librería UniMath, asegurando la corrección y proporcionando una referencia verificada por máquina para la teoría.

Resultados
El artículo demuestra que para diversas clases de categorías univalentes, existe una biequivalencia con las clases correspondientes de categorías de comprensión univalentes. Específicamente:

• Límites Finitos: Categorías univalentes con límites finitos $\simeq$ categorías de comprensión DFL (Unidad, Producto, Ecualizador, $\Sigma$).
• LCCC: LCCC univalentes $\simeq$ categorías de comprensión DFL con tipos $\Pi$.
• Toposes: Toposes elementales univalentes (con/sin NNO) $\simeq$ categorías de comprensión DFL con las propiedades locales correspondientes (por ejemplo, clasificadores de subobjetos, sumas disjuntas, cocientes).
• Universos: Toposes elementales univalentes con un universo cerrado bajo formadores de tipos específicos $\simeq$ categorías de comprensión DFL con un objeto de universo que satisfaga las condiciones de cierre correspondientes.

El artículo demuestra que, en los fundamentos univalentes, el lenguaje interno de estas estructuras categóricas es la teoría de tipos de Martin-Löf extensional. El uso de categorías univalentes simplifica la teoría al eliminar la necesidad de fibraciones partidas y del axioma de elección; los problemas de coherencia que afectan a los modelos de la teoría de conjuntos (donde la sustitución debe ser estricta) se resuelven porque los isomorfismos son identidades.

Significado y Reivindicaciones
El artículo sostiene que su desarrollo proporciona una nueva perspectiva sobre la semántica de la teoría de tipos dependientes. Al utilizar categorías univalentes, el autor evita la carga técnica de las fibraciones partidas y el axioma de elección, que son necesarios en los fundamentos de la teoría de conjuntos para asegurar la corrección (soundness). Los principios de identidad de estructura inherentes a los fundamentos univalentes permiten un tratamiento más natural de las estructuras categóricas donde los objetos se identifican mediante equivalencia en lugar de igualdad estricta.

El autor afirma explícitamente que no construye la sintaxis ni el modelo inicial en este trabajo; más bien, se centra en el lado categórico del teorema del lenguaje interno (la equivalencia entre modelos). Señala que, si bien las categorías de comprensión son adecuadas para los fundamentos univalentes, otras estructuras como las CwF no lo son, debido a la restricción de conjuntos sobre los tipos. El artículo se posiciona como un paso fundacional, dejando el desarrollo de una sintaxis adecuada (como la sintaxis de grupoide) y su interpretación como trabajo futuro. La importancia radica en establecer una correspondencia robusta y verificada por máquina entre las estructuras categóricas univalentes y las teorías de tipos, demostrando que los fundamentos univalentes apoyan naturalmente estos teoremas de lenguaje interno sin los defectos presentes en las formulaciones anteriores de la teoría de conjuntos.