Directed type theory, with a twist

Aquí presento un resumen técnico detallado del artículo "Directed type theory, with a twist" (Teoría de tipos dirigida, con un giro), escrito por Fernando Chu y Paige Randall North.

1. El Problema

La Teoría de Tipos de Homotopía (HoTT) ha tenido un éxito notable como fundamento de las matemáticas y como lenguaje interno para razonar sobre $\infty$-grupoides (espacios). Sin embargo, en muchas áreas de las matemáticas y la informática, las estructuras más relevantes son las categorías, no los grupoides. Los grupoides tienen morfismos invertibles, mientras que las categorías tienen morfismos dirigidos (no necesariamente invertibles).

Aunque se han propuesto varias teorías de tipos dirigidas para abordar esto, muchas existentes fallan en satisfacer tres criterios de diseño fundamentales que permitirían un razonamiento sintáctico similar al de HoTT pero para categorías:

1. Tipos como categorías: Todo tipo en un contexto vacío debería interpretarse semánticamente como una categoría (sin estructuras extra no deseadas).
2. Estructura categórica emergente: Debe existir un tipo de "igualdad dirigida" (tipo Hom) con reglas de formación, introducción, eliminación y computación, que permita codificar celdas $n$-dimensionales y coherencias de manera natural.
3. Igualdades dirigidas triviales a través de objetos de camino: La regla de introducción del tipo Hom debe corresponder a la factorización del mapa diagonal a través de la categoría de flechas ($A^\to$), generalizando la noción de homotopía en HoTT para permitir el razonamiento sobre transformaciones naturales.

La mayoría de las teorías existentes satisfacen solo uno o dos de estos criterios, a menudo sacrificando la simplicidad semántica o la capacidad de razonar sobre transformaciones naturales de manera sintáctica.

2. Metodología

Los autores proponen una nueva teoría llamada Teoría de Tipos Enredados (Twisted Type Theory - TTT). Su metodología se basa en los siguientes pilares:

• Modelo Semántico: Se construye sobre el "modelo de categorías" de North, que interpreta contextos como categorías y tipos como categorías indexadas.
• Nueva Operación Sintáctica (Twist): Introducen una operación novedosa llamada "giro" (twist) sobre los tipos. Dado un tipo que depende tanto contravariante como covariante de ciertas variables, su "giro" produce un nuevo tipo que depende solo covariante de esas mismas variables.
• Semántica de los Giros: Para dar sentido a esta operación, los autores desarrollan la teoría de fibraciones 2-laterales dependientes (D2SFibs). Esta es una generalización de la noción de fibraciones 2-laterales de Street.
  • Demuestran un teorema de enderezado-desenderezado (straightening-unstraightening) para D2SFibs, estableciendo una equivalencia fibrida entre profuntores dependientes y D2SFibs.
  • La interpretación del "giro" de un tipo corresponde a la parte de "desenderezado" de esta equivalencia.
• Reglas Modificadas: Utilizan esta estructura semántica para definir nuevas reglas para los tipos Hom, específicamente una regla de introducción y eliminación que satisface los criterios de diseño.

3. Contribuciones Clave

1. Definición de TTT: Presentan una extensión de la Teoría de Tipos de Martin-Löf (MLTT) que incluye tipos $\Sigma$, $\Pi$, tipos Hom, tipos opuestos, contextos opuestos y, crucialmente, la operación de giro (twist) y tipos mostrados (displayed types).
2. Teoría de D2SFibs: Desarrollan la teoría básica de las fibraciones 2-laterales dependientes y prueban el teorema de straightening-unstraightening, lo cual es un resultado independiente de interés en teoría de categorías.
3. Regla de Introducción Hom: Logran formular una regla de introducción para tipos Hom ($\text{refl}_A^d$) que es análoga sintácticamente a la regla de introducción de identidad en HoTT, pero cuya interpretación semántica es la categoría de flechas $A^\to$. Esto resuelve el problema de las "igualdades dirigidas triviales".
4. Regla de Eliminación Hom: Proponen una regla de eliminación para tipos Hom que generaliza la eliminación de identidad, permitiendo razonar sobre transformaciones naturales. Esta regla se basa en la propiedad de levantamiento de las D2SFibs.
5. Conexión con Estructuras Existentes: Muestran cómo el giro conecta con tipos $\Sigma$ y $\Pi$, y cómo permite caracterizar la opuesta de un tipo $\Sigma$.

4. Resultados Principales

• Validación del Modelo: Demuestran que el modelo de categorías valida todas las reglas de TTT, incluyendo la nueva regla de eliminación de Hom.
• Razonamiento sobre Transformaciones Naturales: Logran capturar sintácticamente la noción semántica de transformaciones naturales entre funtores. Un término del tipo $\text{Hom}(F a, G a)$ (donde $F$ y $G$ son funtores) corresponde a una transformación natural.
• Unicidad Dirigida (Directed Univalence): Establecen una regla de conversión para tipos de funciones entre conjuntos (tipos discretos) que los identifica con tipos Hom, generalizando el principio de identidad de estructura a un contexto dirigido.
• Lema de Yoneda Sintético: Utilizan TTT para proporcionar una prueba sintética del Lema de Yoneda. La prueba demuestra que la eliminación de tipos Hom contiene esencialmente toda la información necesaria para el lema, reorganizando los datos de manera invertible. Esto valida la utilidad de la teoría para razonar sobre categorías de manera interna.

5. Significado e Impacto

El trabajo de Chu y North es significativo porque:

• Cierra la brecha sintáctica-semántica: Proporciona un lenguaje interno donde el razonamiento sobre categorías es tan fluido como el razonamiento sobre espacios en HoTT, sin sacrificar la simplicidad semántica (todos los tipos son categorías).
• Generalización de HoTT: Muestra cómo las técnicas de demostración de HoTT (como la eliminación de identidad) pueden adaptarse al mundo dirigido mediante la noción de "giro" y las D2SFibs.
• Fundamento para Futuras Extensiones: Al mantener una base semántica simple (categorías 1-dimensionales) pero con una sintaxis rica, TTT sirve como un punto de partida sólido para explorar modelos de dimensión superior en el futuro.
• Herramienta Práctica: La capacidad de probar el Lema de Yoneda sintéticamente demuestra que la teoría no es solo teórica, sino que permite realizar matemáticas categóricas constructivas dentro del sistema.

En resumen, Twisted Type Theory ofrece una solución elegante al problema de formalizar la teoría de categorías dentro de la teoría de tipos, introduciendo una operación de "giro" que permite reconciliar la dependencia contravariante y covariante, permitiendo así un razonamiento dirigido robusto y sintácticamente manejable.