🔢 mathematics

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

Este artigo demonstra que a teoria de tipos simpliciais pode ser formulada como teoria de tipos homotópica com um tipo intervalo postulado ao provar que preenchimentos únicos para $(2,1)$ -horns implicam preenchimentos únicos para todos os inner horns via a adjunção de Leibniz na categoria selvagem de tipos, um resultado que foi formalizado em Cubical Agda.

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

Publicado 2026-06-18

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está tentando construir uma cidade complexa e multicamadas onde as estradas não são apenas linhas planas, mas têm direção, regras de trânsito e até "engarrafamentos" que podem ser resolvidos de maneiras específicas. Este artigo é sobre a construção de um conjunto melhor de plantas para essa cidade, especificamente para um mundo matemático chamado Teoria do Tipo de Homotopia (HoTT).

Aqui está o detalhamento do que os autores fizeram, usando analogias simples.

1. O Problema: Construindo uma Cidade com Ruas de Mão Única

Na matemática padrão (e na HoTT padrão), as estradas são como ruas de mão dupla. Se você pode ir de A para B, você sempre pode voltar. É como um grupo de amigos onde todos estão igualmente conectados.

Mas os autores querem construir uma cidade com ruas de mão única (morfismos direcionados). Nesta cidade, você pode ir de A para B, mas talvez não possa voltar. Este é o mundo da Teoria do Tipo Simplicial.

No entanto, há um detalhe: em uma cidade normal, se você tem uma estrada de A para B e outra de B para C, você pode facilmente combiná-las para criar uma estrada de A para C. Mas nesta cidade matemática de alta tecnologia, simplesmente dizer "podemos combiná-las" não é suficiente. Você tem que provar que a combinação funciona perfeitamente e que, se você combinar três estradas em ordens diferentes, você terminará no mesmo lugar.

Na "forma antiga" de fazer isso (o framework de Riehl-Shulman), essas regras eram escritas em uma "metalinguagem" separada (como um livro de regras escrito fora da cidade). Os autores queriam escrever as regras dentro da própria cidade, usando uma ferramenta especial chamada Tipo de Intervalo (pense nisso como uma régua que mede a direção).

2. A Grande Descoberta: A "Adjunção de Leibniz"

O principal feito técnico do artigo é provar uma regra poderosa que eles chamam de Adjunção de Leibniz.

A Analogia: A Máquina de "Empurrar-Puxar"
Imagine que você tem duas máquinas:

A Máquina de Produto-Pushout (O Empurrar): Esta máquina pega duas estradas de mão única e as combina para criar uma nova estrutura de estrada mais complexa. É como pegar dois blocos de Lego e encaixá-los lado a lado para fazer uma base mais larga.
A Máquina de Hom-Pullback (O Puxar): Esta máquina faz o inverso. Ela olha para uma estrutura de estrada complexa e pergunta: "De quantas maneiras posso encaixar uma estrada menor específica dentro desta?" É como perguntar: "De quantas maneiras diferentes posso deslizar uma peça de quebra-cabeça específica dentro deste quebra-cabeça maior?"

Os autores provaram que essas duas máquinas estão perfeitamente ligadas.

Se você sabe como a máquina de "Empurrar" funciona, você automaticamente sabe como a máquina de "Puxar" funciona.
Elas são dois lados da mesma moeda.

Por que isso é difícil?
Normalmente, na matemática simples, esse elo é óbvio. Mas neste mundo matemático "selvagem" (onde as estradas podem girar e mudar de forma infinitamente), provar esse elo é como tentar dar um nó em uma corda que muda de forma constantemente. Os autores tiveram que ser incrivelmente cuidadosos para garantir que os "nós" (as provas matemáticas) permanecessem firmes sem se desfazerem.

3. O Atalho: Mudando de Mapas para Famílias

Um dos truques inteligentes que os autores usaram foi mudar sua perspectiva.

O Jeito Difícil: Tentar provar a regra olhando para "mapas" individuais (estradas específicas de A para B). Isso é como tentar resolver um engarrafamento olhando para cada carro individualmente. Torna-se confuso e bagunçado muito rapidamente.
O Jeito Fácil: Eles perceberam que olhar para "famílias" (grupos de estradas organizados por um ponto de partida) era muito mais limpo. É como observar o fluxo de tráfego de um bairro inteiro em vez de carros individuais.

Eles provaram que o mundo dos "Mapas" e o mundo das "Famílias" são, na verdade, a mesma coisa (graças a uma regra chamada Univalência). Ao mudar para a visão de "Família", o ato de desatar os nós complicados tornou-se muito mais fácil de resolver.

4. O Resultado: Resolvendo o Quebra-Cabeça da "Composição"

Uma vez que a máquina de "Empurrar-Puxar" estava funcionando, eles a aplicaram a um problema específico: Tipos de Segal.

O Problema:
Um "Tipo de Segal" é uma cidade onde você pode combinar estradas (compor). Mas para que a cidade seja estável, você precisa garantir que:

Combinar estradas funciona.
Combiná-las em ordens diferentes produz o mesmo resultado (associatividade).
Toda a "cola" de nível superior que sustenta essas regras é perfeita.

No passado, os matemáticos tinham que verificar essas regras uma por uma, como se estivessem verificando cada tijolo em uma parede.

O Resultado Antigo: Eles sabiam que as primeiras camadas de tijolos eram sólidas (para formas pequenas como triângulos e quadrados).
O Novo Resultado: Os autores usaram sua máquina de "Empurrar-Puxar" para provar que se a primeira camada de tijolos for sólida, então todas as camadas acima dela serão sólidas automaticamente.

Eles mostraram que, se uma cidade possui uma regra simples para combinar duas estradas (uma forma de "chifre"), ela possui automaticamente as regras perfeitas para combinar qualquer número de estradas, não importa quão complexa seja a forma.

5. A "Formalização" (A Prova Computacional)

Finalmente, os autores não escreveram apenas no papel. Eles construíram um modelo digital de toda a sua teoria usando um programa de computador chamado Cubical Agda.

Pense nisso como construir uma simulação virtual da sua cidade.
Eles rodaram o código e o computador verificou cada passo de sua lógica para garantir que não houvesse bugs ou pontas soltas.
Isso prova que a máquina de "Empurrar-Puxar" e o resultado de "todas as camadas são sólidas" são 100% corretos matematicamente.

Resumo

Em resumo, os autores construíram uma nova maneira interna de lidar com "ruas de mão única" na matemática. Eles descobriram uma poderosa relação de "Empurrar-Puxar" entre combinar estradas e analisá-las. Usando essa relação, provaram que, se uma estrutura matemática funciona para formas simples, ela funciona automaticamente para todas as formas complexas, poupando os matemáticos de terem que verificar cada possibilidade manualmente. Eles verificaram tudo isso usando um computador para garantir precisão absoluta.

Resumo Técnico: A Adjunção de Leibniz na Teoria de Tipos Homotópica

Enunciado do Problema
A teoria de tipos simpliciais (STT) estende a teoria de tipos homotópicos (HoTT) para fornecer uma estrutura sintética para categorias superiores, equipando os tipos com morfismos direcionados via um intervalo. Um desafio central neste campo é definir "tipos de Segal" — tipos onde os morfismos direcionados podem ser compostos. Embora a composição seja direta, garantir que essa composição seja associativa e unitária requer uma hierarquia infinita de coerências superiores. Na formulação padrão da STT por Riehl e Shulman, essas coerências são frequentemente tratadas via construções metateóricas, o que torna a formalização completa difícil. Especificamente, provar que um tipo com preenchimentos únicos para $(2,1)$ -cornos (a condição básica para tipos de Segal) implica preenchimentos únicos para todos os cornos $(n,k)$ internos (generalizando a associatividade e a unitalidade da composição) é não trivial. Resultados anteriores, como os de Riele e Shulman, cobriram casos de baixa dimensão específicos ( $n=3$ ), mas uma prova geral para todos os $n$ e $k$ dentro de um framework unificado de HoTT permaneceu como um obstáculo técnico em aberto.

Metodologia
Os autores adotam uma abordagem de teoria de tipos homotópicos "plana", seguindo Gratzer, Weinberger e Buchholtz, em vez da abordagem de intervalo metateórico de Riehl e Shulman. Eles postulam um tipo de intervalo $I$ que forma um reticulado distributivo limitado, evitando a necessidade de ordens totais ou modalidades específicas.

A inovação técnica central é a internalização da adjunção de Leibniz dentro da "categoria selvagem de tipos".

Categorias Selvagens: Os autores trabalham com "categorias selvagens", que são traduções ingênuas da teoria das categorias para HoTT. Estas carecem de dados de coerência superior (as leis de associatividade e identidade ocorrem definicionalmente ou não são rastreadas), tornando-as distintas de $(\infty, 1)$ -categorias, mas suficientes para os propósitos dos autores.
A Adjunção: Eles estabelecem que o produto-pushout (denotado $\hat{\times}$ $\hat{\times}$ ) é adjunto ao pullback-hom (denotado $\pitchfork$ $⋔$ ) na categoria selvagem de aplicações (maps).
- Para aplicações $f: A \to B$ e $g: X \to Y$ , o produto-pushout $f \hat{\times} g$ é a aplicação induzida a partir do pushout de $f \times Y$ e $A \times g$ .
- O pullback-hom $f \pitchfork g$ é a aplicação induzida entre tipos de função.
- A adjunção estabelece: $\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$ .
Aplicações vs. Famílias: Uma prova direta desta adjunção na categoria selvagem de aplicações é intratável devido à complexidade de rastrear dados de coerência (7-uplas de aplicações e identificações). Para superar isso, os autores utilizam o axioma da univalência para estabelecer uma equivalência entre a categoria selvagem de aplicações e a categoria selvagem de famílias (tipos dependentes). Eles provam que o produto-pushout e o pullback-hom correspondem ao join fibrado e a uma construção específica de produto dependente na categoria de famílias, onde a adjunção é mais fácil de verificar.

Principais Contribuições e Resultados

A Adjunção de Leibniz (Teorema 3.16): O artigo prova que o produto-pushout e o pullback-hom formam um par adjunto na categoria selvagem de tipos. Este é um resultado técnico significativo porque, embora bem conhecido para 1-categorias, provar isso para estruturas superiores (mesmo no cenário "selvagem") requer o tratamento cuidadoso da equivalência entre aplicações e famílias para evitar um rastreamento de coerência intratável.
Generalização das Propriedades de Tipo de Segal (Teorema 4.9): Usando a adjunção de Leibniz, os autores provam que, se um tipo possui preenchimentos únicos para $(2,1)$ $(2, 1)$ -cornos (ou seja, é um tipo de Segal), ele automaticamente possui preenchimentos únicos para todos os $(n,k)$ $(n, k)$ -cornos internos ( $0 < k < n$ $0 < k < n$ ).
- Isso generaliza o resultado de Riehl e Shulman (que cobriu $n=3$ ) e fornece uma versão do resultado de Lurie para a teoria de tipos simpliciais.
- A prova baseia-se em mostrar que as inclusões de corno interno $\lambda^n_k$ são "anódinas internas" (ortogonais à esquerda de todos os tipos de Segal). Isso é alcançado demonstrando que $\lambda^n_k$ é um retrato do produto-pushout $\lambda^n_k \hat{\times} \lambda^2_1$ , e então aplicando as propriedades de fechamento de ortogonalidade derivadas da adjunção de Leibniz.
Formalização: Todos os resultados são formalizados em Cubical Agda. O código está disponível e serve como uma verificação dos complexos argumentos combinatórios envolvendo índices e pushouts.

Significância e Alegações
O artigo alega que sua principal contribuição é a bem-sucedida internalização da adjunção de Leibniz dentro de HoTT, o que serve como uma ferramenta poderosa para derivar coerências superiores em teoria de tipos simpliciais.

Framework Sintético: Ao trabalhar com um tipo de intervalo interno, os autores demonstram que todas as coerências superiores para tipos de Segal podem ser enunciadas e derivadas sinteticamente dentro de Hoft, sem recorrer à quantificação metateórica.
Viabilidade de Formalização: Os autores destacam que sua abordagem permite uma formalização completa em Agda. Eles observam que, embora a abordagem metateórica de Rieห์–Shulman possa tornar o enunciado do teorema mais fácil (devido ao raciocínio baseado em conjuntos no nível meta), a prova do caso geral em seu framework interno é não trivial e exigiu o desenvolvimento da adjunção de Leibniz para gerenciar a "maior parte do desafio" referente ao rastreamento de coerência.
Utilidade Técnica: A equivalência entre a categoria selvagem de aplicações e famílias é apresentada como uma ferramenta metodológica crucial que simplifica as provas envolvendo o produto-pushout e o pullback-hom, tornando a derivação de propriedades de ortogonalidade viável.

Em resumo, o artigo fornece uma fundação rigorosa e formalizada para a teoria de tipos simpliciais, provando que a condição básica de Segal implica a coerência categórica superior total através da aplicação da adjunção de Leibniz em um cenário categórico selvagem.