Strict stability of extension types

Resumen Técnico: Estabilidad Estricta de los Tipos de Extensión

Planteamiento del Problema
El artículo aborda una brecha fundacional en el desarrollo sintético de $(\infty, 1)$-categorías dentro de la Teoría de Tipos Homotópicos (HoTT), específicamente el sistema introducido por Riehl y Shulman. Si bien la semántica de este sistema se esbozó utilizando la teoría de homotopía simplicial y el modelo de espacios de Segal, la formulación original dejó abierta la demostración de la estabilidad estricta de los tipos de extensión bajo sustitución. En los modelos de teoría de tipos, la "estabilidad estricta" requiere que la interpretación de los formadores de tipos (como los tipos de extensión) conmute estrictamente con los cuadrados de tracción (sustitución), en lugar de hacerlo meramente hasta isomorfismo o homotopía. Sin esta propiedad, el sistema no puede interpretarse plenamente en el lenguaje interno de un $\infty$-topos de una manera que soporte la igualdad estricta requerida para ciertas teorías de categorías internas (por ejemplo, las de Martini–Wolf).

Metodología
El autor emplea el método de división (splitting method) originalmente descrito por Voevodsky y posteriormente generalizado por Lumsdaine y Warren para universos locales. El enfoque implica los siguientes pasos técnicos:

1. Categorías de Universos: El trabajo se sitúa dentro de una categoría de universo (una categoría $\mathcal{C}$ equipada con un objeto universo $U$ y una fibración universal $\pi: \tilde{U} \to U$). El autor asume la existencia de una "división" (splitting), que es una elección global de cuadrados de tracción para la fibración universal. Esto asegura que el reindexado (sustitución) se modele mediante la igualdad estricta de objetos y morfismos, no solo mediante isomorfismo.
2. Contextos Genéricos: Siguiendo el estilo del trabajo de Awodey sobre modelos naturales, el artículo define contextos genéricos (objetos clasificadores) para la formación e introducción de tipos de extensión.
   • $U_{\text{Ext}@j}$ se define como el objeto que clasifica pares de una familia de tipos $A$ y una sección parcial $a$ sobre una inclusión de forma $j: \phi \hookrightarrow \psi$.
   • $U_{\lambda@j}$ se define como el objeto que clasifica triples $\langle A, a, b \rangle$ donde $b$ es una extensión total de $a$.
3. Construcción de Tracción Estricta: El autor construye el formador de tipo de extensión $\text{Ext}@j$ y el mapa de introducción $\lambda@j$ como morfismos entre estos contextos genéricos y el universo. Al utilizar la división de la fibración universal, el artículo demuestra que el cuadrado formado por estos mapas es un pullback estricto (no solo un pullback débil).
4. Supuestos de Fibrancia: Para simplificar el entorno técnico manteniendo la aplicabilidad a modelos estándar (objetos simpliciales en un $\infty$-topos), el autor asume que las "formas" (los contextos simpliciales) son fibrantes. Esto asegura que los cotensores de Leibniz sean fibraciones, permitiendo que los tipos de extensión se modelen como pullbacks ordinarios de 1-categoría.

Contribuciones Clave y Resultados
La contribución principal es el Teorema 3.8, que establece la estabilidad estricta de los tipos de extensión. El teorema demuestra que para un topos de tipos $\mathcal{E}$ y su asociado modelo simplicial $s\mathcal{E}$, una división fija de los formadores de tipos estándar produce una interpretación de los tipos de extensión que satisface las siguientes igualdades estrictas para cualquier morfismo de contexto $\sigma: \Delta \to \Gamma$:

1. Estabilidad de Formación: $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. Estabilidad de Introducción: $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. Estabilidad de Eliminación: $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

El artículo detalla además cómo se satisfacen las reglas de computación $\beta$ y $\eta$ dentro de este marco de estabilidad estricta, apoyándose en la propiedad universal de los cuadrados de pullback definidos por la división.

Significancia y Reivindicaciones
El artículo afirma que este resultado resuelve el problema abierto de la estabilidad estricta de los tipos de extensión en el sistema de Riehl–Shulman. El resultado práctico es que el sistema posee ahora una semántica robusta en los objetos simpliciales de un $\infty$-topos. Esto permite el uso del sistema para demostrar teoremas sobre $\infty$-categorías internas en el sentido de Martini–Wolf, ya que la estabilidad estricta asegura que las operaciones de la teoría de tipos se alineen perfectamente con los pullbacks categóricos requeridos para la teoría de categorías internas.

El autor señala que, si bien el trabajo asume un único universo y formas fibrantes para simplificación técnica, se cree que el razonamiento se generaliza a jerarquías de universos y estructuras fibradas más complejas sin obstrucciones esenciales. El trabajo sirve como un puente entre la sintaxis sintética de la HoTT simplicial y la semántica rigurosa de los $\infty$-topoi.