Univalent Enriched Categories and the Enriched Rezk Completion

Resumen Técnico: Categorías Enriquecidas Univalentes y la Completitud de Rezk Enriquecida

Planteamiento del Problema
La teoría de categorías es un marco fundacional para las matemáticas y las ciencias de la computación, donde las categorías enriquecidas desempeñan un papel crítico en la teoría de categorías superiores, la teoría de homotopía y la semántica de los lenguajes de programación (por ejemplo, utilizando DCPOs para lenguajes con efectos). Sin embargo, dentro del contexto de los Fundamentos Univalentes (Teoría de Tipos Homotópicos), la definición estándar de categorías a menudo falla en satisfacer el principio de equivalencia, que establece que los objetos isomórfos deben ser indistinguibles. Si bien se han establecido "categorías univalentes" (donde la identidad de los objetos es equivalente al isomorfismo) para las categorías ordinarias, la teoría de las categorías enriquecidas univalentes permanece insuficientemente desarrollada. Específicamente, existe una falta de resultados formalizados respecto al principio de identidad de la estructura, la caracterización de las equivalencias y la existencia de una completitud de Rezk (una reflexión univalente) para las categorías enriquecidas. Además, construcciones estándar como las categorías de Kleisli a menudo no son univalentes, lo que requiere un método para construir análogos univalentes dentro del entorno enriquecido.

Metodología
El artículo desarrolla la teoría de las categorías enriquecidas dentro del asistente de pruebas Rocq utilizando la biblioteca UniMath, adhiriéndose a los Fundamentos Univalentes. El enfoque metodológico central involucra:

1. El Enriquecimiento como Estructura: En lugar de definir las categorías enriquecidas como una colección de objetos y objetos-hom (la definición de Kelly), los autores las definen como una categoría junto con un enriquecimiento. Un enriquecimiento consiste en objetos-hom en una categoría monoidal $\mathcal{V}$, morfismos de identidad y composición, y una correspondencia entre los morfismos en la categoría subyacente y los elementos de los objetos-hom. Esta perspectiva trata a una categoría enriquecida como una categoría univalente dotada de estructura adicional.
2. Bicategorías Desplegadas: Para probar el principio de identidad de la estructura, los autores utilizan la maquinaria de las bicategorías desplegadas. Definen una bicatégoria desplegada $dEnrichCat_{\mathcal{V}}$ sobre la bicatégoria de las categorías univalentes ($UnivCat$). La bicatégoria total de este despliegue es $EnrichCat_{\mathcal{V}}$. Esto permite la reutilización de los resultados de univalencia existentes para $UnivCat$ para probar la univalencia en el entorno enriquecido.
3. Sistemas de Factorización Ortogonal: Para caracterizar las equivalencias, el artículo emplea sistemas de factorización ortogonal en bicategorías. Define los functores enriquecidos totalmente fieles y esencialmente sobreyectivos y demuestra que forman un sistema de factorización ortogonal.
4. Dos Construcciones de la Completitud de Rezk: El artículo proporciona dos construcciones distintas para la completitud de Rezek de una categoría enriquecida:
   • Inmersión de Yoneda: Construir la completitud como la imagen de la inmersión de Yoneda enriquecida. Esto requiere que $\mathcal{V}$ sea completa y simétrica monoidal cerrada, pero se basa en la teoría de categorías estándar.
   • Tipos Inductivos Superiores (HITs): Construir la completitud dotando a la completitud de Rezk de la categoría subyacente de un enriquecimiento utilizando las reglas de eliminación de los HITs. Este enfoque evita las suposiciones de completitud o cerradura en $\mathcal{V}$ y preserva los niveles de universo si el universo es cerrado bajo HITs.
5. Propiedades Universales: El artículo establece la propiedad universal de la completitud de Rezk, demostrando que la precomposición con una equivalencia débil (functor totalmente fiel y esencialmente sobreyectivo) induce una equivalencia adjunta entre las categorías de functores.

Contribuciones Clave y Resultados

• Principio de Identidad de la Estructura: El artículo demuestra que la bicatégoria de las categorías enriquecidas univalentes ($EnrichCat_{\mathcal{V}}$) es univalente (Teorema 2.8). Esto implica que el tipo de identidad entre dos categorías enriquecidas univalentes es equivalente al tipo de equivalencias adjuntas entre ellas.
• Caracterización de Equivalencias: Se demuestra que todo functor enriquecido que es tanto totalmente fiel como esencialmente sobreyectivo es una equivalencia adjunta (Teorema 4.8). Este resultado es constructivo y depende de que el dominio y el codominio sean univalentes, evitando el axioma de elección.
• Completitud de Rezk: Se proporcionan dos construcciones para la completitud de Rezk de una categoría enriquecida (Construcciones 5.5 y 5.7). El artículo demuestra que toda categoría enriquecida admite una completitud de Rezk y satisface la propiedad universal de que cualquier functor hacia una categoría univalente enriquecida se extiende de forma única a lo largo de equivalencias débiles (Teorema 5.2).
• Categorías de Kleisli Univalentes: Los autores construyen categorías de Kleisli enriquecidas univalentes. Definen la categoría de Kleisli estándar $K(T)$ y su contraparte univalente $Kleisli(T)$ (como un subobjeto completo de la categoría de Eilenberg-Moore). Utilizando la completitud de Rezk y la propiedad universal, muestran que $Kleisli(T)$ satisface la propiedad universal de los objetos de Kleisli en la bicatégoria de las categorías enriquecidas univalentes (Construcción 6.9).
• Ejemplos y Caracterizaciones: El artículo proporciona numerosos ejemplos, incluyendo el auto-enriquecimiento, los enriquecimientos opuestos y los cambios de base. Caracteriza los enriquecimientos sobre estructuras cartesianas (como los DCPOs) e introduce una noción de "estructura cerrada que soporta productos smash", aunque señala limitaciones respecto a los conjuntos apuntados, introduciendo la noción de "estructura cerrada que soporta productos smash" para manejar conjuntos apuntados y posets, aunque nota limitaciones respecto a los DCPOs apuntados.

Significancia y Reivindicaciones
El artículo afirma establecer una base robusta para la teoría de categorías enriquecidas dentro de los Fundamentos Univalentes. Su principal significancia radica en:

1. Formalización: Proporcionar una biblioteca formalizada en Rocq/UniMath para las categorías enriquecidas, que previamente carecía de una formalización extensa en comparación con las categorías ordinarias.
2. Corrección de la Noción: Demostrar que ver las categorías enriquecidas como categorías univalentes con estructura adicional (vía enriquecimientos) simplifica las pruebas de propiedades fundamentales como el principio de identidad de la estructura.
3. Resolución de la No-Univalencia: Abordar el problema de que las construcciones comunes (como las categorías de Kleisli) no son inherentemente univalentes, proporcionando un método sistemático (completitud de Rezk) para obtener versiones univalentes que preservan las propiedades universales necesarias.
4. Herramientas Fundacionales: Establecer la bicatégoria de las categorías enriquecidas univalentes como una bicatégoria univalente, lo cual es un prerrequisito para desarrollar la teoría de categorías interna posterior (por ejemplo, monadas, límites) en un entorno univalente.

Los autores señalan que, si bien su enfoque cubre muchos casos estándar, tiene limitaciones respecto a los productos smash para ciertas estructuras (como los DCPOs apuntados) donde los cocientes deben tomarse en la categoría apropiada en lugar de en conjuntos. Sugieren que el trabajo futuro podría involucrar el desarrollo del equipo de las categorías enriquecidas o la generalización de la noción de producto smash para manejar estos casos.