Univalence without function extensionality

1. Planteamiento del Problema

El artículo aborda una pregunta fundamental en la Teoría de Tipos de Homotopía (HoTT) sobre la relación lógica entre la Univalencia (UA) y la Extensionalidad de Funciones (FE).

• Antecedentes: Es un teorema estándar (debido a Voevodsky) que en cualquier universo univalente, se cumple la extensionalidad de funciones. Es decir, si dos funciones son homotópicas ($f \sim g$), son iguales ($f = g$).
• La Pregunta: ¿Se cumple la recíproca? Específicamente, ¿una forma más débil de univalencia, que afirma que el universo forma una "categoría salvaje univalente" (donde la igualdad de tipos corresponde a la existencia de inversos estrictos, es decir, equivalencias categóricas), implica la extensionalidad de funciones?
• Contexto: François G. Dorais propuso un debilitamiento llamado Univalencia Categórica (CUA), donde el mapa desde la igualdad de tipos hacia la equivalencia categórica (mapas con inversos izquierdos y derechos estrictos) es una equivalencia. Los autores investigan si la CUA implica la FE.

2. Metodología

Los autores emplean la construcción de modelos polinomiales de Von Glehn ($Poly(\mathcal{C})$) para construir un contraejemplo. Este método es una fuente conocida de modelos para la Teoría de Tipos de Martin-Löf (ITT) que refutan la extensionalidad de funciones.

• Modelo Base ($\mathcal{C}$): Comienzan con un modelo $\mathcal{C}$ de ITT que satisface la Univalencia y la Extensionalidad de Funciones (por ejemplo, un modelo cúbico) y posee coproductos finitos extensivos que satisfacen reglas $\eta$ estrictas.
• Construcción del Modelo Polinomial: Construyen el modelo polinomial $Poly(\mathcal{C})$. En este modelo:
  • Los tipos son pares $(S, P)$ que representan "formas" y "posiciones".
  • La construcción está relacionada con la interpretación Dialectica de Gödel y la categoría de contenedores.
  • Crucialmente, se sabe que $Poly(\mathcal{C})$ siempre refuta la FE.
• Análisis de Isomorfismos: El trabajo técnico central implica analizar la estructura de los isomorfismos (equivalencias categóricas) dentro del modelo polinomial. Los autores descomponen el tipo de isomorfismos entre dos tipos en el modelo polinomial en:
  1. Isomorfismos entre sus componentes de "forma" (en el modelo base $\mathcal{C}$).
  2. Isomorfismos entre sus componentes de "posición", condicionados al isomorfismo de forma.

3. Definiciones y Conceptos Clave

• Categoría Salvaje: Una estructura que captura la naturaleza $(\infty, 1)$-categórica de los tipos, donde la composición y las identidades satisfacen leyes de coherencia hasta la igualdad (no necesariamente hasta la homotopía).
• Equivalencia Categórica ($A \sim= B$): Un mapa $f: A \to B$ equipado con inversos izquierdos y derechos estrictos ($sf = id, fs = id$). Esto difiere de una equivalencia homotópica ($A \simeq B$), donde los inversos existen solo hasta la homotopía.
• Univalencia Categórica (CUA): El principio de que el mapa $(A = B) \to (A \sim= B)$ es una equivalencia.
• Univalencia Categórica Familiar (CUA$^\bullet$): Una variante más fuerte que afirma que, para cualquier tipo índice $I$, la categoría de familias indexadas por $I$ es univalente en sentido categórico.
• Descomposición de la Univalencia: El artículo establece que la Univalencia estándar (UA) es lógicamente equivalente a la conjunción de Univalencia Categórica (CUA) y Extensionalidad de Funciones (FE).
  $$UA \iff (CUA \land FE)$$

4. Contribuciones y Resultados Clave

A. Independencia de la CUA y la FE

El resultado principal es la prueba de que la Univalencia Categórica Familiar no implica la Extensionalidad de Funciones.

• Teorema: $ITT + CUA^\bullet_U \nvdash FE_U$.
• Estrategia de Prueba:
  1. Tomar un modelo base $\mathcal{C}$ que satisfaga $UA + FE$.
  2. Construir $Poly(\mathcal{C})$.
  3. Preservación de la CUA: Los autores prueban (Teorema 4.17) que si el modelo base $\mathcal{C}$ satisface la Univalencia Categórica Familiar, entonces el modelo polinomial $Poly(\mathcal{C})$ también la satisface. Esto se basa en el hecho de que los isomorfismos en el modelo polinomial están determinados por los isomorfismos en el modelo base (formas) y condiciones específicas sobre las posiciones que son contractibles cuando el modelo base es univalente.
  4. Refutación de la FE: Es una propiedad conocida de los modelos polinomiales (Proposición 5.3) que refutan la Extensionalidad de Funciones.
  5. Conclusión: $Poly(\mathcal{C})$ es un modelo de $ITT + CUA^\bullet_U + \neg FE_U$.

B. Jerarquía de Variantes de Univalencia

El artículo explora el paisaje de los axiomas de univalencia debilitados, mostrando que no son todos equivalentes:

• CUA vs. CUA$^\bullet$: Los autores muestran que la CUA (para un solo universo) no implica la Univalencia Categórica Familiar (CUA$^\bullet$). Construyen un modelo de rebanada donde la CUA se cumple pero la CUA$^\bullet$ falla.
• Univalencia Categórica Categórica (CCUA): Definen una variante donde el mapa $(A=B) \to (A \sim= B)$ es una equivalencia categórica en lugar de una equivalencia homotópica. Muestran que esto es estrictamente más fuerte que la CUA, pero aún así no implica la FE.
• Univalencia Aproximada: Discuten la "univalencia aproximada" de Van den Berg (existencia de un camino para cada equivalencia) y notan que su relación con la FE sigue siendo una pregunta abierta, aunque los modelos polinomiales refutan una "mejora de equivalencia aproximada" relacionada.

5. Significado

• Desacoplamiento de Axiomas: El artículo demuestra que la propiedad de "univalencia" de un universo puede separarse de la propiedad de "extensionalidad de funciones". Esto desafía la intuición de que la univalencia es un axioma monolítico que fuerza todos los principios de extensionalidad.
• Insight Estructural: Al mostrar que la Univalencia se factoriza en Univalencia Categórica y Extensionalidad de Funciones, los autores proporcionan una comprensión estructural más clara de lo que hace que el axioma de univalencia "funcione". Sugiere que las funciones son "privilegiadas" en la declaración estándar de la univalencia específicamente debido a la interacción con la FE.
• Teoría de Modelos: El trabajo valida la construcción de modelos polinomiales como una herramienta poderosa para separar axiomas sutiles en la teoría de tipos, extendiendo su utilidad más allá de la simple refutación de la FE hacia el análisis de la estructura interna de la univalencia.
• Implicaciones Fundamentales: Para los constructivistas e investigadores fundamentales, esto sugiere que se puede adoptar una forma de univalencia (univalencia categórica) que preserva la equivalencia estructural de los tipos sin comprometerse con el principio más fuerte y históricamente difícil de integrar de la extensionalidad de funciones.

En resumen, el artículo resuelve la pregunta de Dorais de manera negativa: La Univalencia Categórica es estrictamente más débil que la Univalencia completa y no implica la Extensionalidad de Funciones.