Extension Types for Free

Resumen Técnico: Tipos de Extensión "Gratuitos": Cofibraciones, Pegado y Univalencia en la Teoría de Tipos de Dos Niveles

Planteamiento del Problema
Los tipos de extensión son un concepto fundamental en la teoría de tipos dependientes, que aparecen en diversos contextos como las teorías de tipos cúbicos (caminos con extremos fijos), la teoría de tipos simpliciales de Riehl y Shulman (términos fijos sobre subformas), o mecanismos de despliegue controlado. En los marcos existentes, estos tipos suelen postularse como nuevos primitivos, gobernados por un "cálculo de caras" meta-teórico o una capa de forma que dicta su formación y reglas. Este enfoque suele requerir construcciones de modelos específicas o adiciones axiomáticas para validar las reglas (tales como condiciones de frontera estrictas, extensionalidad de funciones relativa y la propiedad de extensión de homotopía). Un problema abierto central en la teoría de tipos homotópicos (HoTT) es determinar la relación precisa entre el "Book HoTT" (la formulación axiomática del libro de HoTT) y las teorías de tipos cúbicos, particularmente si son extensiones conservativas entre sí.

Metodología
El artículo utiliza la Teoría de Tipos de Dos Niveles (2LTT) como un marco unificador. La 2LTT enriquece a HoTT con un nivel "estricto" (externo) de igualdad que satisface la Unicidad de la Prueba de Identidad (UIP) y la extensionalidad de funciones, mientras que el nivel "interno" (fibrante) conserva la estructura homotópica estándar.

• Semántica: El marco es semánticamente "libre"; los modelos estándar de HoTT (por ejemplo, conjuntos simpliciales, conjuntos cúbicos) producen automáticamente modelos de 2LTT mediante construcciones de presheaves. La teoría es conservadora sobre su nivel interno, lo que significa que no se pueden probar nuevos teoremas en el lenguaje interno que no fueran ya demostrables en HoTT.
• Definición de Tipos de Extensión: En lugar de postular tipos de extensión, el artículo los define internamente dentro de 2LTT. Dada una cofibración $i: \Phi \hookrightarrow \Psi$ (un mapa en el nivel externo), una familia fibrante $A$ sobre $\Psi$, y una sección parcial $a$, el tipo de extensión se define como la fibra estricta del mapa de restricción sobre $a$:
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  Aquí, $=_s$ denota la igualdad estricta del nivel externo.
• Cofibraciones: El "cálculo de caras" es reemplazado por la clase de cofibraciones en el nivel externo. El artículo trata la elección específica de qué mapas son cofibraciones como un parámetro, permitiendo que el marco se adapte a diferentes entornos (simpliciales, cúbicos, etc.) sin cambiar la definición central.

Contribuciones Clave y Resultados

1. Tipos de Extensión "Gratuitos":
   El artículo demuestra que, en 2LTT, todo el cálculo de tipos de extensión propuesto por Riehl y Shulman es definible en lugar de axiomático.

   • Reglas Estrictas: Las reglas de introducción, eliminación, $\beta$, $\eta$ y de frontera se cumplen estrictamente por construcción.
   • Axiomas Demostrables: Los axiomas que se postulan en otros entornos, como la extensionalidad de funciones relativa y la propiedad de extensión de homotopía (realineación), se convierten en teoremas derivados de las propiedades de las cofibraciones y fibraciones en 2LTT.
   • Unificación: Esta única definición subsume varias instancias existentes, incluyendo los caminos cúbicos, los tipos de extensión de Riehl-Shulman y los tipos indexados por proposiciones (despliegue controlado).

2. Equivalencia de Pegado y Univalencia:
   El artículo establece un ciclo preciso de implicaciones que conecta el pegado cúbico y el axioma de univalencia dentro del marco de 2LTT:

   • Univalencia $\implies$ Pegado: Si el universo interno es univalente, entonces para cualquier cofibración, el tipo de "Datos de Glue" (estructuras requeridas para formar un tipo Glue) es contractible. Esto implica la existencia de una estructura de Glue que satisfaga las reglas en forma homotópica.
   • Pegado $\implies$ Univalencia: Inversamente, la existencia de una "estructura de Glue débil" (que requiere solo igualdades internas para el acuerdo de fronteras y una estructura de intervalo de caminos) implica que el universo es univalente.
   • Resultado: En presencia de un intervalo de caminos, la univalencia y la existencia de datos de Glue contractibles son equivalentes. Esto revierte la dirección estándar de la implicación (que los tipos Glue implican Univalencia) y establece una equivalencia bidireccional.

3. Formalización:
   Todos los resultados desde la Sección 2 hasta la Sección 5 están auto-formalizados en Agda utilizando la bandera --two-level. La formalización combina argumentos de HoTT internos con razonamiento externo sobre el nivel estricto, verificando la consistencia y corrección de las afirmaciones teóricas.

4. Enfoque hacia la Conservatividad:
   El artículo propone una estrategia para abordar el problema abierto de si las teorías de tipos cúbicos son conservadoras sobre el Book HoTT. Al representar ambas teorías dentro de 2LTT:

   • Book HoFF es representado como MLTT + Univalencia (nivel interno).
   • Teoría de Tipos Cúbicos es representada como MLTT + Glue + Intervalo de Caminos (supuestos estructurales/externos).
   • El artículo demuestra que, sobre una teoría base con un intervalo de caminos, el axioma de Univalencia y el axioma de Glue son inter-derivables. Esto sugiere que la diferencia central entre las teorías puede ser estructural en lugar de lógica, ofreciendo una vía para demostrar la conservatividad.

Significado y Reivindicaciones
El artículo afirma que el marco de 2LTT proporciona una base "gratuita" y uniforme para los tipos de extensión, eliminando la necesidad de axiomas ad-hoc o construcciones de modelos específicos para validar sus reglas. Al internalizar el cálculo de caras como cofibraciones, la teoría unifica diversas ocurrencias de tipos de extensión encontradas en la literatura.

Respecto a la conexión entre las teorías de tipos cúbicos y el Book HoTT, el artículo es modesto. No pretende haber resuelto la conjetura de la conservatividad. En su lugar, ofrece una prueba de concepto: demuestra que el mecanismo central de la teoría de tipos cúbicos (pegado) es lógicamente equivalente al núcleo del axioma de HoTT (univalencia) cuando se observa a través de la lente de 2LTT. Esta equivalencia permite a los investigadores traducir extensiones estructurales (como los tipos Glue) en extensiones axiomáticas dentro de un único marco, facilitando la comparación y pavimentando potencialmente el camino para futuras pruebas de conservatividad. El artículo señala explícitamente que el supuesto de un "intervalo de caminos" en el lado de HoTT sigue siendo un desafío abierto para lograr una equivalencia completa.