A type theory for invertibility in weak $ω$-categories

Aquí presento un resumen técnico detallado del artículo "A type theory for invertibility in weak 𝜔-categories" (Una teoría de tipos para la invertibilidad en 𝜔-categorías débiles), escrito por Thibaut Benjamin, Camil Champin e Ioannis Markakis.

1. El Problema

La teoría de tipos homotópica (HoTT) ha establecido que cada tipo posee la estructura de un ∞-grupoide débil. Basándose en esto, Finster y Mimram introdujeron CaTT (Categorical Type Theory), una teoría de tipos para 𝜔-categorías débiles (categorías infinitas donde la asociatividad y la unidad son válidas solo hasta coherencia de dimensión superior).

Sin embargo, un desafío fundamental en la teoría de las 𝜔-categorías es la formalización de la invertibilidad.

• En categorías ordinarias, un morfismo es invertible si tiene un inverso estricto.
• En bicategorías, esto se relaja a la existencia de 2-células invertibles.
• En 𝜔-categorías, la invertibilidad debe entenderse coinductivamente: demostrar que una célula es invertible requiere producir una cantidad infinita de datos (inversos, unitarios, coherencias de orden superior, etc.).

El problema principal es que la teoría CaTT original no internaliza esta estructura de invertibilidad de manera sintáctica. Aunque se pueden definir células invertibles semánticamente, CaTT carece de constructores de tipos y términos para razonar directamente sobre estas estructuras infinitas dentro del sistema de tipos. Esto dificulta la formalización de conceptos clave como las equivalencias débiles y las equifibraciones, que son esenciales para construir una estructura de modelo en el contexto de 𝜓-categorías débiles.

2. Metodología

Los autores proponen ICaTT, una extensión conservativa de CaTT diseñada para internalizar la invertibilidad coinductiva. La metodología se basa en los siguientes pilares:

• Extensión Sintáctica: Se introduce un nuevo constructor de tipo Inv(A)(t) que representa la estructura de invertibilidad sobre un término t.
• Constructores y Destructores:
  • Destructores: Permiten extraer datos de una estructura de invertibilidad: inversos izquierdo (linv) y derecho (rinv), unitarios (lunit, runit) y sus propias estructuras de invertibilidad (ilunit, irunit).
  • Constructores:
    • inv: Construye una estructura de invertibilidad a partir de datos explícitos.
    • can (Canonical): Internaliza un teorema semántico que establece que si las células de dimensión superior en un diagrama de pegado son invertibles, entonces la célula coherente resultante también lo es.
    • rec: Un recursor que permite definir estructuras de invertibilidad recursivamente, manejando la naturaleza infinita de los datos mediante hipótesis inductivas en el contexto.
• Suspensión: Se extiende la operación de suspensión de CaTT a la nueva sintaxis, permitiendo elevar construcciones de invertibilidad a dimensiones superiores.
• Implementación: Los autores desarrollaron un prototipo de asistente de pruebas para ICaTT, implementando algoritmos de unificación y normalización para manejar la complejidad de los términos.

3. Contribuciones Clave

1. Definición de ICaTT: Una teoría de tipos dependiente que añade tipos de invertibilidad coinductiva a CaTT, manteniendo la capacidad de describir 𝜔-categorías débiles.
2. Conservatividad: Se demuestra que ICaTT es una extensión conservativa de CaTT. Esto significa que cualquier tipo o término válido en CaTT sigue siendo válido en ICaTT sin añadir nuevas igualdades entre términos que no fueran ya válidos en CaTT. La inclusión entre sus categorías sintácticas es fiel y plena.
3. La "Walking Equivalence" (Equivalencia Caminante): Se demuestra que el contexto E1 en ICaTT (que clasifica estructuras de invertibilidad) corresponde semánticamente a la "walking equivalence" de Ozornova y Rovelli. Esto permite caracterizar las equifibraciones (análogos a las isofibraciones) como morfismos con la propiedad de elevación derecha respecto a ciertas inclusiones.
4. Semántica en 𝜔-Categorías Marcadas: Se generaliza la noción de 𝜔-categorías marcadas (donde ciertas células están "marcadas" para indicar invertibilidad) al caso débil. Se construye una semántica de ICaTT en la categoría de 𝜔-categorías marcadas fibrantes, donde las células marcadas son exactamente aquellas que poseen una estructura de invertibilidad coinductiva.
5. Normalización: Se analiza el sistema de reescritura de ICaTT. Aunque el sistema no termina (debido a la naturaleza coinductiva de la invertibilidad), se prueba que es normalizable para tipos y términos "categóricos" (aquellos que no dependen de la estructura de invertibilidad), lo que permite la verificación de tipos.

4. Resultados Principales

• Formalización de Propiedades de Invertibilidad: Utilizando ICaTT, los autores formalizaron resultados clásicos sobre células invertibles con esfuerzo mínimo, demostrando que:
  • La composición de células invertibles es invertible.
  • Los inversos izquierdo y derecho de una célula invertible son a su vez invertibles.
  • Existe una célula invertible entre el inverso izquierdo y el derecho.
  • Las células invertibles satisfacen la propiedad 2-de-6 (si $f, g, h$ son componibles y $f*g$ y $g*h$ son invertibles, entonces $f, g, h$ lo son).
• Construcción de la Semántica: Se define un functor $L: \text{Mod}(\text{ICaTT}) \to \omega\text{Cat}^+_{\text{fibrant}}$ que asigna a cada modelo de ICaTT una 𝜔-categoría marcada fibrante. En esta semántica, una célula está marcada si y solo si es la imagen de un morfismo que clasifica una estructura de invertibilidad.
• Relación con Modelos Existentes: Se establece una conexión directa entre los modelos de ICaTT y la caracterización de las equifibraciones propuesta por Fujii et al., utilizando la "walking equivalence" como contexto base.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

• Puente entre Sintaxis y Semántica: Proporciona un marco sintáctico riguroso para razonar sobre estructuras infinitas (invertibilidad) en el contexto de categorías débiles, algo que antes requería razonamiento metateórico complejo o definiciones semánticas ad hoc.
• Avance hacia Estructuras de Modelo: La construcción de una semántica en 𝜔-categorías marcadas fibrantes es un paso crucial hacia la demostración de la existencia de una estructura de modelo (model structure) para las 𝜔-categorías débiles, un problema abierto de larga data en la teoría de homotopía superior.
• Herramienta Práctica: La implementación de ICaTT como asistente de pruebas permite a los investigadores formalizar y verificar propiedades de alta dimensión que eran anteriormente inaccesibles o extremadamente tediosas de manejar manualmente.
• Generalización de Conceptos: Extiende el trabajo de Henry y Loubaton sobre 𝜔-categorías marcadas al caso débil, ofreciendo una noción más flexible de invertibilidad que evita las restricciones de los ∞-grupoide estrictos.

En resumen, ICaTT representa un avance fundamental en la formalización de la teoría de categorías de dimensión superior, proporcionando las herramientas necesarias para tratar la invertibilidad como una estructura de primera clase dentro de un sistema de tipos, lo que abre la puerta a nuevas investigaciones sobre la estructura homotópica de las 𝜔-categorías.