🔢 mathematics

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Este artículo demuestra que la teoría de tipos simpliciales puede formularse como teoría de tipos homotópicos con un tipo intervalo postulado al probar que los llenadores únicos para cuernos $(2,1)$ implican llenadores únicos para todos los cuernos internos a través de la adjunción de Leibniz en la categoría salvaje de tipos, un resultado que ha sido formalizado en Cubical Agda.

Autores originales: Tom de Jong, Nicolai Kraus, Axel Ljungström

Publicado 2026-06-18

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Tom de Jong, Nicolai Kraus, Axel Ljungström

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

Imagina que estás intentando construir una ciudad compleja y de múltiples niveles donde las carreteras no son solo líneas planas, sino que tienen dirección, reglas de tráfico e incluso "atascos de tráfico" que pueden resolverse de formas específicas. Este artículo trata sobre la construcción de un mejor conjunto de planos para esa ciudad, específicamente para un mundo matemático llamado Teoría de Tipos de Homotopía (HoTT).

Aquí está el desglose de lo que hicieron los autores, utilizando analogías sencillas.

1. El Problema: Construir una ciudad con calles de un solo sentido

En las matemáticas estándar (y en la HoTT estándar), las carreteras son como calles de doble sentido. Si puedes ir del punto A al punto B, siempre puedes volver. Es como un grupo de amigos donde todos están igualmente conectados.

Pero los autores quieren construir una ciudad con calles de un solo sentido (morfismos dirigidos). En esta ciudad, puedes ir de A a B, pero tal vez no de regreso. Este es el mundo de la Teoría de Tipos Simpliciales.

Sin embargo, hay un detalle: en una ciudad normal, si tienes una carretera de A a B y otra de B a C, puedes combinarlas fácilmente para crear una carretera de A a C. Pero en esta ciudad matemática de alta tecnología, simplemente decir "podemos combinarlas" no es suficiente. Tienes que demostrar que la combinación funciona perfectamente, y que si combinas tres carreteras en diferentes órdenes, terminas en el mismo lugar.

En la "vieja" forma de hacer esto (el marco de Riehl-Shulman), estas reglas se escribían en un "metalenguaje" separado (como un libro de reglas escrito fuera de la ciudad). Los autores querían escribir las reglas dentro de la ciudad misma, usando una herramienta especial llamada Tipo de Intervalo (piensa en ello como una regla que mide la dirección).

2. El Gran Descubrimiento: La "Adjunción de Leibniz"

El principal logro técnico del artículo es demostrar una regla poderosa que llaman la Adjunción de Leibniz.

La Analogía: La máquina de "Empujar-Tirar"
Imagina que tienes dos máquinas:

La Máquina de Producto-Pushout (El Empuje): Esta máquina toma dos carreteras de un solo sentido y las combina para crear una nueva estructura de carretera más compleja. Es como tomar dos piezas de Lego y encajarlas una al lado de la otra para hacer una base más ancha.
La Máquina de Hom-Pullback (El Tirón): Esta máquina hace lo contrario. Observa una estructura de carretera compleja y pregunta: "¿De cuántas maneras puedo encajar una carretera más pequeña específica dentro de esta?". Es como preguntar: "¿De cuántas maneras diferentes puedo deslizar una pieza de rompecabezas específica dentro de este rompecabezas más grande?".

Los autores demostraron que estas dos máquinas están perfectamente vinculadas.

Si sabes cómo funciona la máquina de "Empuje", automáticamente sabes cómo funciona la máquina de "Tirón".
Son dos caras de la misma moneda.

¿Por qué es esto difícil?
Normalmente, en las matemáticas simples, este vínculo es obvio. Pero en este mundo matemático "salvaje" (donde las carreteras pueden retorcerse y girar de infinitas maneras), demostrar este vínculo es como intentar hacer un nudo en una cuerda que no deja de cambiar de forma. Los autores tuvieron que ser increíblemente cuidadosos para asegurar que los "nudos" (las pruebas matemáticas) se mantuvieran unidos sin desmoronarse.

3. El Atajo: Cambiar de Mapas a Familias

Uno de los trucos ingeniosos que usaron los autores fue cambiar su perspectiva.

La Forma Difícil: Intentar demostrar la regla mirando mapas individuales (carreteras específicas de A a B). Esto es como intentar arreglar un atasco de tráfico mirando cada coche individualmente. Se vuelve desordenado y confuso muy rápido.
La Forma Fácil: Se dieron cuenta de que mirar "familias" (grupos de carreteras organizados por un punto de partida) era mucho más limpio. Es como observar el flujo de tráfico de todo un vecindario en lugar de los coches individuales.

Demostraron que el mundo de los "Mapas" y el mundo de las "Familias" son en realidad lo mismo (gracias a una regla llamada Univalencia). Al cambiar a la vista de "Familia", el enredo desordenado se volvió mucho más fácil de resolver.

4. El Resultado: Resolviendo el Rompecabezas de la "Composición"

Una vez que hicieron que su máquina de "Empuje-Tirón" funcionara, la aplicaron a un problema específico: Tipos Segal.

El Problema:
Un "Tipo Segal" es una ciudad donde sí puedes combinar carreteras (componer). Pero para que la ciudad sea estable, necesitas asegurar que:

Combinar carreteras funciona.
Combinarlas en diferentes órdenes da el mismo resultado (asociatividad).
Todo el "pegamento" de niveles superiores que sostiene estas reglas es perfecto.

En el pasado, los matemáticos tenían que verificar estas reglas una por una, como si revisaran cada ladrillo en una pared.

El Resultado Anterior: Sabían que las primeras capas de ladrillos eran sólidas (para formas pequeñas como triángulos y cuadrados).
El Nuevo Resultado: Los autores usaron su máquina de "Empuje-Tirón" para demostrar que si la primera capa de ladrillos es sólida, entonces todas las capas superiores son sólidas automáticamente.

Demostraron que si una ciudad tiene una regla simple para combinar dos carreteras (una forma de "cuerno"), automáticamente tiene las reglas perfectas para combinar cualquier número de carreteras, sin importar lo complejo que sea el diseño.

5. La "Formalización" (La Prueba Computacional)

Finalmente, los autores no solo escribieron esto en papel. Construyeron un modelo digital de toda su teoría utilizando un programa de computadora llamado Cubical Agda.

Piensa en esto como construir una simulación virtual de su ciudad.
Ejecutaron el código y la computadora verificó cada paso de su lógica para asegurar que no hubiera errores o cabos sueltos.
Esto demuestra que su máquina de "Empuje-Tirón" y su resultado de "todas las capas son sólidas" son matemáticamente 100% correctos.

Resumen

En resumen, los autores construyeron una nueva forma interna de manejar "calles de un solo sentido" en las matemáticas. Descubrieron una poderosa relación de "Empuje-Tirón" entre combinar carreteras y analizarlas. Usando esta relación, demostraron que si una estructura matemática funciona para formas simples, automáticamente funciona para todas las formas complejas, ahorrando a los matemáticos el tener que verificar cada posibilidad a mano. Verificaron todo esto usando una computadora para asegurar una precisión absoluta.

Resumen Técnico: La Adjunción de Leibniz en la Teoría de Tipos Homotópica

Planteamiento del Problema
La teoría de tipos simpliciales (STT) extiende la teoría de tipos homotópica (HoTT) para proporcionar un marco sintético para categorías superiores mediante el equipamiento de tipos con morfismos dirigidos a través de un intervalo. Un desafío central en este campo es definir los "tipos Segal"—tipos donde los morfismos dirigidos pueden componerse. Si bien la composición es sencilla, asegurar que esta composición sea asociativa y unitaria requiere una jerarquía infinita de coherencias superiores. En la formulación estándar de la STT de Riehl y Shulman, estas coherencias suelen manejarse mediante construcciones metateóricas, lo que dificulta la formalización completa. Específicamente, demostrar que un tipo con llenados únicos para $(2,1)$ -horns (la condición básica para los tipos Segal) implica llenados únicos para todos los $(n,k)$ -horns internos (generalizando la asociatividad y la unitariedad de la composición) no es trivial. Resultados previos, como los de Riehl y Shulman, cubrieron casos de baja dimensión específicos ( $n=3$ ), pero una prueba general para todos los $n$ y $k$ dentro de un marco unificado de HoTT seguía siendo un obstáculo técnico abierto.

Metodología
Los autores adoptan un enfoque de teoría de tipos homotópica "plana", siguiendo a Gratzer, Weinberger y Buchholtz, en lugar del enfoque de intervalo metateórico de Riehl y Shulman. Postulan un tipo de intervalo $I$ que forma un reticulado distributivo acotado, evitando la necesidad de órdenes totales o modalidades específicas.

La innovación técnica central es la internalización de la adjunción de Leibniz dentro de la "categoría salvaje de tipos".

Categorías Salvajes: Los autores trabajan con "categorías salvajes", que son traducciones ingenuas de la teoría de categorías a HoTT. Estas carecen de datos de coherencia superior (las leyes de asociatividad e identidad se cumplen de forma definicional o no se rastrean), lo que las hace distintas de las $(\infty, 1)$ -categorías, pero suficientes para los propósitos de los autores.
La Adjunción: Establecen que el producto de pushout (denotado $\hat{\times}$ $\hat{\times}$ ) es adjunto al hom-pullback (denotado $\pitchfork$ $⋔$ ) en la categoría salvaje de aplicaciones.
- Para las aplicaciones $f: A \to B$ y $g: X \to Y$ , el producto de pushout $f \hat{\times} g$ es la aplicación inducida desde el pushout de $f \times Y$ y $A \times g$ .
- El hom-pullback $f \pitchfork g$ es la aplicación inducida entre tipos de funciones.
- La adjunción establece: $\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$ .
Aplicaciones vs. Familias: Una prueba directa de esta adjunción en la categoría salvaje de aplicaciones es intratable debido a la complejidad de rastrear los datos de coherencia (7-tuplas de aplicaciones e identificaciones). Para superar esto, los autores utilizan el axioma de univalencia para establecer una equivalencia entre la categoría salvaje de aplicaciones y la categoría salvaje de familias (tipos dependientes). Prueban que el producto de pushout y el hom-pullback corresponden a la unión por fibra (fiberwise join) y a una construcción específica de producto dependiente en la categoría de familias, donde la adjunción es más fácil de verificar.

Contribuciones Clave y Resultados

La Adjunción de Leibniz (Teorema 3.16): El artículo demuestra que el producto de pushout y el hom-pullback forman un par adjunto en la categoría salvaje de tipos. Este es un resultado técnico significativo porque, si bien es bien conocido para 1-categorías, demostrarlo para estructuras superiores (incluso en el entorno "salvaje") requiere un manejo cuidadoso de la equivalencia entre aplicaciones y familias para evitar un intratable registro de coherencia.
Generalización de las Propiedades de los Tipos Segal (Teorema 4.9): Utilizando la adjunción de Leibniz, los autores demuestran que si un tipo tiene llenados únicos para $(2,1)$ $(2, 1)$ -horns (es decir, es un tipo Segal), automáticamente tiene llenados únicos para todos los $(n,k)$ $(n, k)$ -horns internos ( $0 < k < n$ $0 < k < n$ ).
- Esto generaliza el resultado de Riehl y Shulman (que cubría $n=3$ ) y proporciona una versión del resultado de Lurie para la teoría de tipos simpliciales.
- La prueba se basa en demostrar que las inclusiones de horn internos $\lambda^n_k$ son "anodinas internas" (izquierda ortogonales a todos los tipos Segal). Esto se logra demostrando que $\lambda^n_k$ es un retracto del producto de pushout $\lambda^n_k \hat{\times} \lambda^2_1$ , y luego aplicando las propiedades de clausura de la ortogonalidad derivadas de la adjunción de Leibniz.
Formalización: Todos los resultados están formalizados en Cubical Agda. El código está disponible y sirve como verificación de los complejos argumentos combinatorios que involucran índices y pushouts.

Significancia y Reivindicaciones
El artículo afirma que su contribución principal es la exitosa internalización de la adjunción de Leibniz dentro de HoTT, lo cual sirve como una herramienta poderosa para derivar coherencias superiores en la teoría de tipos simpliciales.

Marco Sintético: Al trabajar con un tipo de intervalo interno, los autores demuestran que todas las coherencias superiores para los tipos Segal pueden enunciarse y derivarse sintéticamente dentro de HoTT, sin recurrir a la cuantificación metateórica.
Viabilidad de la Formalización: Los autores destacan que su enfoque permite una formalización completa en Agda. Observan que, si bien el enfoque metateórico de Riehl–Shulman podría facilitar el enunciado del teorema (debido al razonamiento basado en conjuntos a nivel metateórico), la prueba del caso general en su marco interno es no trivial y requirió el desarrollo de la adjunción de Leibniz para gestionar la "mayoría abrumadora del desafío" respecto al seguimiento de la coherencia.
Utilidad Técnica: La equivalencia entre la categoría salvaje de aplicaciones y familias se presenta como una herramienta metodológica crucial que simplifica las pruebas que involucran el producto de pushout y el hom-pullback, haciendo que la derivación de las propiedades de ortogonalidad sea factible.

En resumen, el artículo proporciona una base rigurosa y formalizada para la teoría de tipos simpliciales, demostrando que la condición básica de Segal implica la coherencia categórica superior completa mediante la aplicación de la adjunción de Leibniz en un entorno categórico salvaje.