💻 computer science

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

Este artículo construye modelos de conjuntos materiales no bien fundados en la Teoría de Tipos Homotópicos que satisfacen los Axiomas de Anti-Fundación de Scott y Aczel mediante M-tipos y coálgebras terminales, extiende estos axiomas a niveles de tipos superiores dentro de la Teoría de Conjuntos Materiales Univalente, y proporciona una caracterización de los tipos de identidad de M-tipos, con todos los resultados formalizados en Agda.

Autores originales: Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

Publicado 2026-07-01

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

La visión general: Construyendo un universo de conjuntos "giratorios"

Imagina que estás construyendo un universo de objetos (conjuntos). En la forma tradicional de hacer matemáticas (llamada teoría de conjuntos "bien fundada"), cada objeto se construye a partir de objetos más pequeños, que a su vez se construyen a partir de otros aún más pequeños, todo el camino hasta llegar a la nada. Es como una pirámide: no puedes tener un bloque flotando en el aire; debe descansar sobre algo debajo de él.

Pero, ¿qué pasaría si quisieras construir un universo donde las cosas pudieran descansar sobre sí mismas? ¿Qué pasaría si tuvieras una caja que se contiene a sí misma? ¿O una cadena de cajas donde la Caja A está dentro de la Caja B, que está dentro de la Caja C, que a su vez está dentro de la Caja A? En las matemáticas tradicionales, esto está prohibido porque crea un bucle infinito. En este artículo, los autores exploran cómo construir un universo matemático que permita estos bucles, utilizando un marco moderno llamado Teoría de Tipos Homotópicos (HoTT).

El artículo hace dos cosas:

Construye un modelo de conjuntos que permite bucles, siguiendo las reglas establecidas por un matemático llamado Scott.
Construye un modelo diferente de conjuntos que permite bucles, siguiendo las reglas establecidas por un matemático llamado Aczel.

Las herramientas: Árboles, Coálgebras y "Desplegar"

Para entender sus modelos, imagina un árbol.

Árboles bien fundados (la forma antigua) son como árboles genealógicos. Tienen una raíz, ramas y, eventualmente, terminan en hojas. Dejan de crecer.
Árboles no bien fundados (la nueva forma) pueden ser como un fractal o una sala de espejos. Una rama puede volver sobre sí misma y convertirse de nuevo en la raíz. O una rama puede dividirse en dos ramas idénticas que se ven exactamente iguales al árbol completo.

Los autores utilizan un concepto llamado Coálgebras para describir estos árboles. Piensa en una coálgebra como una "máquina" que te dice cómo mirar un nodo y ver qué viene después.

Si la máquina dice "detente", tienes una hoja.
Si la máquina dice "ve a estos hijos", tienes ramas.
Si la máquina dice "ve a un hijo que es en realidad tú mismo", tienes un bucle.

El artículo pregunta: ¿Cuál es la "máquina definitiva" que puede describir todos los bucles posibles?

Los dos modelos: Scott vs. Aczel

Los autores construyen dos "máquinas definitivas" diferentes (modelos matemáticos) para manejar estos bucles. Estas corresponden a dos filosofías diferentes sobre cómo tratar la igualdad en estos mundos con bucles.

1. El modelo del "Espejo" (El Axioma de No Fundación de Scott)

La analogía: Imagina una sala de espejos. Si te paras frente a un espejo, ves un reflejo. Si ese reflejo está en otro espejo, ves un reflejo de un reflejo.
La regla: En este modelo, dos objetos se consideran "iguales" si sus patrones de despliegue se ven iguales. Si sigues abriendo las capas de un conjunto (como pelar una cebolla o desplegar un árbol), y el patrón de ramas es idéntico al de otro conjunto, son el mismo.
El resultado: Los autores construyeron un tipo específico de estructura de árbol (llamada $V^0_\infty$ ) que actúa como este modelo. Es un "punto fijo", lo que significa que si aplicas las reglas del universo a este, obtienes el mismo universo de vuelta.
Hallazgo clave: Este modelo no es la máquina "final" o "terminal" en el sentido más estrico. Es una "tercera opción": no es el punto de partida (inicial) ni el punto final absoluto (terminal). Se sitúa en el medio. Cumple con las reglas de Scott, que son más estrictas sobre cómo se identifican los bucles.

2. El modelo "Universal" (El Axioma de No Fundación de Aczel)

La analogía: Imagina un catálogo maestro de todas las historias posibles que podrías contar, incluyendo historias que se cuentan a sí mismas.
La regla: En este modelo, cualquier grafo (un dibujo de puntos y líneas) puede convertirse en un conjunto. Si tienes un dibujo de un bucle, hay un conjunto único que coincide perfectamente con ese dibujo.
El resultado: Los autores construyeron una "Coálgebra Terminal" (la máquina definitiva) para este propósito. Sin embargo, para construir esta máquina específica, tuvieron que utilizar una herramienta matemática especial y algo controvertida llamada Redimensionamiento Proposicional (Propositional Resizing).
- ¿Qué es el Redimensionamiento Proposicional? Imagina que tienes una biblioteca gigante de libros (proposiciones). Esta herramienta te permite encoger toda la biblioteca para que quepa en un solo estante, sin perder ninguna de las historias. Es un atajo poderoso que hace posible la construcción.
Hallazgo clave: Este modelo cumple con las reglas de Aczel. Es el objeto "terminal", lo que significa que es la versión más completa posible de un universo de conjuntos con bucles bajo estas reglas.

El rompecabezas de la "Identidad": ¿Qué hace que dos cosas sean lo mismo?

Una parte importante del artículo es resolver un rompecabezas complicado: ¿Cómo sabemos cuándo dos árboles con bucles son en realidad el mismo?

En las matemáticas estándar, si dos cosas se ven iguales, son iguales. Pero en un mundo con bucles, las cosas se vuelcen extrañas.

Los autores descubrieron que la "igualdad" entre dos puntos en sus árboles con bucles puede describirse como otro tipo de árbol (un "M-tipo indexado").
La metáfora: Imagina que estás comparando dos fractales infinitos. Para demostrar que son iguales, no solo miras la imagen completa; tienes que comparar cada una de las ramas, y cada sub-rama, y cada sub-sub-rama. El artículo proporciona una receta precisa (una "caracterización") de cómo hacer esta comparación. Demostraron que la "igualdad" de estos bucles complejos es, en sí misma, un objeto estructurado e infinito.

Resumen de logros

El Modelo de Scott: Construyeron un universo de conjuntos que permite bucles, donde la igualdad se determina por la forma del árbol de "despliegue". Este modelo es un punto fijo pero no es el "terminal" absoluto.
El Modelo de Aczel: Construyeron el universo "definitivo" de conjuntos que permite bucles, donde cualquier grafo puede convertirse en un conjunto. Esto requirió un supuesto matemático especial (el Redimensionamiento Proposicional).
La receta de la "Igualdad": Descubrieron exactamente cómo definir la "mismidad" para estas estructuras infinitas y con bucles, mostrando que la igualdad es simplemente otro tipo de estructura de árbol.
Formalización: No solo escribieron esto en papel; lo construyeron dentro de un programa informático llamado Agda, que verifica cada paso lógico para asegurar que no haya errores.

¿Por qué es esto importante?

El artículo no pretende resolver problemas de ingeniería del mundo real o cuestiones médicas. En cambio, resuelve un enigma fundamental en las matemáticas. Demuestra que podemos construir un universo lógico y consistente donde los "círculos" y los "bucles" están permitidos, utilizando el lenguaje moderno de la Teoría de Tipos Homotópicos. Une la brecha entre la teoría de conjuntos clásica (que prohíbe los bucles) y la lógica de la informática moderna (que necesita manejar estructuras de datos complejas y circulares como flujos de datos o sistemas de transición).

En resumen: construyeron dos "universos" diferentes donde las cosas pueden contenerse a sí mismas, demostraron que funcionan según reglas específicas y mostraron exactamente cómo determinar si dos de estas cosas que se contienen a sí mismas son en realidad la misma.

Resumen Técnico: Coálgebras Terminales y Conjuntos No Bien Fundados en la Teoría de Tipos Homotópicos

Planteamiento del Problema
El artículo aborda el desafío de modelar conjuntos materiales no bien fundados dentro de la Teoría de Tipos Homotópicos (HoTT). Mientras que la teoría de conjuntos bien fundados ha sido modelada con éxito en HoFF utilizando tipos inductivos superiores (donde la igualdad es el tipo identidad), el modelado de conjuntos no bien fundados —conjuntos que pueden contenerse a sí mismos o formar cadenas de membresía infinitas— ha dependido históricamente de los setoids (donde la igualdad es una relación binaria separada) en lugar del tipo identidad. Los autores pretenden construir modelos de conjuntos no bien fundados en HoTT donde la igualdad se interprete estrictamente como el tipo identidad, integrando así nociones clásicas de la coálgebra universal y la teoría de conjuntos no bien fundados en las estructuras de mayor dimensión que soporta HoTT. Específicamente, el artículo busca construir coálgebras terminales para functores de conjunto potencia restringidos para modelar el Axioma de Anti-Fundación (AFA) de Aczel y construir puntos fijos alternativos que modelen el Axioma de Anti-Fundación de Scott (SAFA).

Metodología
Los autores emplean el marco de la Teoría de Conjuntos Materiales Univalentes y la teoría de coálgebras para endofunctores salvajes sobre el universo de tipos. La metodología involucra tres enfoques técnicos primarios:

Dualización de Conjuntos Iterativos: Los autores construyen una jerarquía de tipos $V^n_\infty$ mediante la dualización de la construcción de conjuntos iterativos ( $V^n$ ). Mientras que $V^n$ es el álgebra inicial del functor de conjunto potencia restringido $P^n$ , $V^n_\infty$ se construye como un subtipo específico del M-tipo (el coálgebra terminal del functor de conjunto potencia no restringido $P^\infty$ ). Este subtipo se define mediante un predicado coinductivo que asegura que los mapas de ramificación en cada nodo estén truncados a un nivel específico.
Caracterización de los Tipos Identidad: Un paso técnico crucial es la caracterización de los tipos identidad de los M-tipos. Los autores demuestran que el tipo identidad entre dos elementos de un M-tipo es equivalente a un M-tipo indexado (específicamente, el coálgebra terminal de un functor polinomial indexado derivado del "despliegue" de una relación). Esta caracterización es esencial para demostrar la pequeña escala local (local smallness) de los modelos construidos.
Adaptación de la Construcción de Aczel–Mendler: Para construir una verdadera coálgebra terminal para el functor de conjunto potencia restringido $P^0$ $P^{0}$ (que modela AFA), los autores adaptan el clásico teorema de Aczel–Mendler a la teoría de tipos. Esta adaptación requiere:
- Definir functors "basados en U" (functores donde los valores sobre tipos grandes son colímites de valores sobre tipos pequeños).
- Utilizar el levantamiento de relaciones (relation lifting) y el concepto de "precongruencias" para realizar el cociente de la coálgebra débilmente terminal.
- Asumir el redimensionamiento proposicional (propositional resizing) para asegurar que los tipos cociente resultantes sean localmente pequeños y que la construcción se mantenga para functores con valores de conjunto como $P^0$ .

Contribuciones Clave y Resultados

Un Modelo del Axioma de Anti-Fundación de Scott (SAFA): Los autores construyen un tipo $V^0_\infty$ que es un punto fijo del functor de conjunto potencia restringido $P^0$ , pero que no es ni el álgebra inicial ni la coálgebra terminal. Demuestran que este tipo, equipado con la relación de pertenencia inducida, satisface el Axioma de Anti-Fundación de Scott. En este modelo, la igualdad es el tipo identidad, y el modelo es "simple" (cualquier par de homomorfismos hacia él son iguales) pero no terminal.
Generalización a Tipos Superiores: La construcción se generaliza a una jerarquía $V^n_\infty$ para cualquier nivel de truncamiento $n$ . Estos modelos satisfacen los axiomas $k$ -SAFA generalizados para todo $k \le n$ . El artículo demuestra que estos modelos satisfacen axiomas de la teoría de conjuntos estándar (conjunto vacío, separación, unión, etc.) en los niveles de truncamiento apropiados, siempre que los modelos sean localmente pequeños.
Caracterización de los Tipos Identidad de M-tipos: El artículo proporciona una caracterización completa del tipo identidad de los M-tipos como M-tipos indexados (Teorema 2.15). Este resultado se utiliza para demostrar que los modelos construidos son localmente pequeños, una condición necesaria para que sirvan como modelos válidos de la teoría de conjuntos materiales en HoTT.
Un Modelo del Axioma de Anti-Fundación de Aczel (AFA): Asumiendo el axioma de redimensionamiento proposicional, los autores construyen una coálgebra terminal para el functor de conjunto potencia restringido $P^0$ (y más generalmente para functores basados en $U$ ). Esta coálgebra terminal sirve como un modelo de la AFA de Aczel, donde cada grafo tiene una decoración única.
No Terminalidad de $V^0_\infty$ : El artículo demuestra explícitamente que $V^0_\infty$ no es la coálgebra terminal para $P^0$ . Proporciona un contraejemplo que muestra que pueden existir homomorfismos de coálgebra distintos desde un grafo específico hacia $V^0_\infty$ , distinguiéndolo de la coálgebra terminal construida mediante el método de Aczel–Mendler.

Significado y Reivindicaciones
El artículo afirma proporcionar los primeros modelos de conjuntos materiales no bien fundados en HoTT donde la igualdad es el tipo identidad, yendo más allá de los modelos basados en setoids del pasado.

Distinción entre AFA y SAFA: El trabajo clarifica la relación entre los axiomas de anti-fundación de Aczel y de Scott dentro del contexto de HoTT. Muestra que, mientras que la coálgebra terminal (que requiere redimensionamiento proposicional) valida AFA, el punto fijo co-iterativo (construible sin redimensionamiento) valida SAFA. Los autores señalan que en el caso no truncado ( $\infty$ ), AFA y SAFA coinciden, pero divergen en niveles de truncamiento inferiores.
Naturaleza Constructiva: La construcción del modelo SAFA ( $V^n_\infty$ ) es totalmente constructiva y no depende de axiomas impredicativos como el redimensionamiento proposicional.
Formalización: Todos los resultados principales están formalizados en el asistente de pruebas Agda, utilizando tanto Agda estándar como Cubical Agda (para la Sección 6), asegurando la corrección de los complejos argumentos homotópicos.
Preguntas Abiertas: Los autores señalan modestamente que la existencia de la coálgebra terminal para $P^0$ sin redimensionamiento proposicional sigue siendo una pregunta abierta. No pretenden haber resuelto si tal construcción es posible o si su existencia implica principios clásicos, sino que lo destacan como una motivación primaria para trabajos futuros.

En resumen, el artículo extiende con éxito la teoría de los conjuntos no bien fundados al entorno de dimensiones superiores de HoTT, proporcionando modelos distintos para diferentes axiomas de anti-fundación y estableciendo la base técnica necesaria respecto a los M-tipos y las estructuras de coálgebra.