💻 computer science

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

Este artigo constrói modelos de conjuntos materiais não-bem-fundados em Teoria dos Tipos Homotópicos que satisfazem os Axiomas de Anti-Fundação de Scott e de Aczel via M-tipos e coálgebras terminais, estende estes axiomas para níveis de tipos superiores dentro da Teoria dos Conjuntos Materiais Univalentes, e fornece uma caracterização dos tipos de identidade de M-tipos, com todos os resultados formalizados em Agda.

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

Publicado 2026-07-01

📖 7 min de leitura🧠 Leitura aprofundada

CC BY 4.0

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

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

A Visão Geral: Construindo um Universo de Conjuntos "Giratórios"

Imagine que você está construindo um universo de objetos (conjuntos). Da maneira tradicional de fazer matemática (chamada de teoria de conjuntos "bem-fundamentada"), cada objeto é construído a partir de objetos menores, que são construídos a partir de outros ainda menores, até chegar ao nada. É como uma pirâmide: você não pode ter um bloco flutuando no ar; ele deve repousar sobre algo abaixo dele.

Mas e se você quiser construir um universo onde as coisas podem repousar sobre si mesmas? E se você tiver uma caixa que contém a si mesma? Ou uma corrente de caixas onde a Caixa A está dentro da Caixa B, que está dentro da Caixa C, que está dentro da Caixa A? Na matemática tradicional, isso é proibido porque cria um loop infinito. Neste artigo, os autores exploram como construir um universo matemático que permite esses loops, usando uma estrutura moderna chamada Teoria do Tipo de Homotopia (HoTT).

O artigo faz duas coisas:

Constrói um modelo de conjuntos que permite loops, seguindo as regras estabelecidas pelo matemático Scott.
Constrói um modelo diferente de conjuntos que permite loops, seguindo as regras estabelecidas pelo matemático Aczel.

As Ferramentas: Árvores, Coalgebras e o "Desdobrar"

Para entender seus modelos, imagine uma árvore.

Árvores bem-fundamentadas (a maneira antiga) são como árvores genealógicas. Elas têm uma raiz, ramos e, eventualmente, terminam em folhas. Elas param de crescer.
Árvores não-bem-fundamentadas (a maneira nova) podem ser como um fractal ou uma sala de espelhos. Um ramo pode retornar e tornar-se a própria raiz novamente. Ou um ramo pode se dividir em dois ramos idênticos que parecem exatamente com a árvore inteira.

Os autores usam um conceito chamado Coalgebras para descrever essas árvores. Pense em uma coalgebra como uma "máquina" que lhe diz como olhar para um nó e ver o que vem a seguir.

Se a máquina diz "parar", você tem uma folha.
Se a máquina diz "vá para estes filhos", você tem ramos.
Se a máquina diz "vá para um filho que é, na verdade, você", você tem um loop.

O artigo pergunta: Qual é a "máquina definitiva" que pode descrever todos os loops possíveis?

Os Dois Modelos: Scott vs. Aczel

Os autores constrom dois diferentes "máquinas definitivas" (modelos matemáticos) para lidar com esses loops. Eles correspondem a duas filosofias diferentes sobre como tratar a igualdade nesses mundos de loops.

1. O Modelo "Espelho" (O Axioma da Não-Fundação de Scott)

A Analogia: Imagine uma sala de espelhos. Se você ficar de frente para um espelho, vê um reflexo. Se esse reflexo estiver em outro espelho, você vê um reflexo de um reflexo.
A Regra: Neste modelo, dois objetos são considerados "iguais" se seus padrões de desdobramento parecerem iguais. Se você continuar abrindo as camadas de um conjunto (como descascar uma cebola ou desdobrar uma árvore), e o padrão de ramos for idêntico ao de outro conjunto, eles são o mesmo.
O Resultado: Os autores construíram um tipo específico de estrutura de árvore (chamada $V^0_\infty$ ) que atua como este modelo. É um "ponto fixo", o que significa que, se você aplicar as regras do universo a ele, você obtém o mesmo universo de volta.
Descoberta Principal: Este modelo não é a máquina "final" ou "terminal" no sentido mais estrito. É uma "terceira opção" — não é o ponto de partida (inicial) e nem o ponto final absoluto (terminal). Ele está no meio. Ele satisfaz as regras de Scott, que são mais rigorosas sobre como os loops são identificados.

2. O Modelo "Universal" (O Axioma da Não-Fundação de Aczel)

A Analogia: Imagine um catálogo mestre de todas as histórias que você poderia contar, incluindo histórias que contam a si mesmas.
A Regra: Neste modelo, qualquer grafo (uma imagem de pontos e linhas) pode ser transformado em um conjunto. Se você tem a imagem de um loop, existe um conjunto único que corresponde perfeitamente a essa imagem.
O Resultado: Os autores construíram uma "Coalgebra Terminal" (a máquina definitiva) para este propósito. No entanto, para construir esta máquina específica, eles tiveram que usar uma ferramenta matemática especial e um tanto controversa chamada Redimensionamento Proposicional (Propositional Resizing).
- O que é Redimensionamento Proposicional? Imagine que você tem uma biblioteca gigante de livros (proposições). Esta ferramenta permite que você encolha a biblioteca inteira para que ela caiba em uma única prateleira, sem perder nenhuma das histórias. É um atalho poderoso que torna a construção possível.
Descoberta Principal: Este modelo satisfaz as regras de Aczel. É o objeto "terminal", o que significa que é a versão mais completa possível de um universo de conjuntos de loops sob estas regras.

O Enigma da "Identidade": O Que Torna Duas Coisas Iguais?

Uma parte importante do artigo é resolver um enigma complicado: Como sabemos quando duas árvores de loop são realmente as mesmas?

Na matemática padrão, se duas coisas parecem iguais, elas são iguais. Mas em um mundo com loops, as coisas ficam estranhas.

Os autores descobriram que a "igualdade" entre dois pontos em suas árvores de loop pode ser descrita como outro tipo de árvore (um "M-tipo indexado").
A Metáfora: Imagine que você está comparando dois fractais infinitos. Para provar que são os mesmos, você não olha apenas para a imagem inteira; você tem que comparar cada um dos ramos, cada sub-ramo, cada sub-sub-ramo. O artigo fornece uma receita precisa (uma "caracterização") de como fazer essa comparação. Eles provaram que a "igualdade" desses loops complexos é, ela própria, um objeto estruturado e infinito.

Resumo das Conquistas

O Modelo de Scott: Eles construíram um universo de conjuntos que permite loops, onde a igualdade é determinada pela forma da árvore de "desdobramento". Este modelo é um ponto fixo, mas não é o "terminal" absoluto.
O Modelo de Aczel: Eles construíram o universo "definitivo" de conjuntos que permite loops, onde qualquer grafo pode ser transformado em um conjunto. Isso exigiu uma suposição matemática especial (Redimensionamento Proposicional).
A Receita da "Igualdade": Eles descobriram exatamente como definir a "mesmidade" para essas estruturas infinitas e em loop, mostrando que a igualdade é apenas outro tipo de estrutura de árvore.
Formalização: Eles não apenas escreveram isso no papel; eles construíram isso dentro de um programa de computador chamado Agda, que verifica cada passo lógico para garantir que não haja erros.

Por Que Isso Importa?

O artigo não afirma resolver problemas de engenharia do mundo real ou questões médicas. Em vez disso, ele resolve um enigma fundamental da matemática. Ele mostra que podemos construir um universo lógico e consistente onde "círculos" e "loops" são permitidos, usando a linguagem moderna da Teoria do Tipo de Homotopia. Ele faz a ponte entre a teoria de conjuntos clássica (que proíbe loops) e a lógica da ciência da computação moderna (que precisa lidar com estruturas de dados circulares complexas, como fluxos de dados/streams e sistemas de transição).

Em resumo: Eles construíram dois "universos" diferentes onde as coisas podem conter a si mesmas, provaram que eles funcionam de acordo com regras específicas e mostraram exatamente como dizer se duas dessas coisas que se contêm são, de fato, a mesma coisa.

Resumo Técnico: Coálgebras Terminais e Conjuntos Não-Bem-Fundados em Teoria de Tipos Homotópica

Enunciado do Problema
O artigo aborda o desafio de modelar conjuntos materiais não-bem-fundados dentro da Teoria de Tipos Homotópica (HoTT). Enquanto a teoria de conjuntos bem-fundados foi modelada com sucesso em HoTT usando tipos indutivos superiores (onde a igualdade é o tipo de identidade), a modelagem de conjuntos não-bem-fundados — conjuntos que podem conter a si mesmos ou formar cadeias de pertinência infinitas — historicamente dependeu de setoids (onde a igualdade é uma relação binária separada) em vez do tipo de identidade. Os autores visam construir modelos de conjuntos não-bem-fundados em HoTT onde a igualdade é interpretada estritamente como o tipo de identidade, integrando assim noções clássicas de coálgebra universal e teoria de conjuntos não-bem-fundados nas estruturas de maior dimensão suportadas pela HoTT. Especificamente, o artigo busca construir coálgebras terminais para funtores de conjunto das partes restritos para modelar o Axioma da Anti-Fundação de Aczel (AFA) e construir pontos fixos alternativos modelando o Axioma da Anti-Fundação de Scott (SAFA).

Metodologia
Os autores empregam o framework da Teoria de Conjuntos Materiais Univalentes e a teoria de coálgebras para funtores endomorfos selvagens no universo de tipos. A metodologia envolve três abordagens técnicas primárias:

Dualização de Conjuntos Iterativos: Os autores constroem uma hierarquia de tipos $V^n_\infty$ ao dualizar a construção de conjuntos iterativos ( $V^n$ ). Enquanto $V^n$ é o álgebra inicial do funtor de conjunto das partes restrito $P^n$ , $V^n_\infty$ é construído como um subtipo específico do M-tipo (o coálgebra terminal do funtor de conjunto das partes irrestrito $P^\infty$ ). Este subtipo é definido por um predicado coindutivo que garante que os mapas de ramificação em cada nó sejam truncados para um nível específico.
Caracterização de Tipos de Identidade: Um passo técnico crucial envolve a caracterização dos tipos de identidade de M-tipos. Os autores provam que o tipo de identidade entre dois elementos de um M-tipo é equivalente a um M-tipo indexado (especificamente, o coálgebra terminal de um funtor polinomial indexado derivado do "desdobramento" de uma relação). Esta caracterização é essencial para provar a pequena localidade (local smallness) dos modelos construídos.
Adaptação da Construção de Aczel–Mendler: Para construir um verdadeiro coálgebra terminal para o funtor de conjunto das partes restrito $P^0$ $P^{0}$ (que modela o AFA), os autores adaptam o clássico teorema de Aczel–Mendler para a teoria de tipos. Esta adaptação requer:
- Definir funtores "baseados em U" (funtores onde os valores em tipos grandes são colimites de valores em tipos pequenos).
- Utilizar levantamento de relação (relation lifting) e o conceito de "precongruências" para realizar o quociente do coálgebra fracamente terminal.
- Assumir redimensionamento proposicional (propositional resizing) para garantir que os tipos quocientes resultantes sejam localmente pequenos e que a construção se mantenha para funtores com valores de conjunto como $P^0$ .

Contribuições Principais e Resultados

Um Modelo do Axioma da Anti-Fundação de Scott (SAFA): Os autores constroem um tipo $V^0_\infty$ que é um ponto fixo do funtor de conjunto das partes restrito $P^0$ , mas que não é nem a álgebra inicial nem o coálgebra terminal. Eles provam que este tipo, equipado com a relação de pertinência induzida, satisfaz o Axioma da Anti-Fundação de Scott. Neste modelo, a igualdade é o tipo de identidade, e o modelo é "simples" (qualquer dois homomorfismos para ele são iguais), mas não terminal.
Generalização para Tipos Superiores: A construção é generalizada para uma hierarquia $V^n_\infty$ para qualquer nível de truncamento $n$ . Estes modelos satisfazem os axiomas $k$ -SAFA generalizados para todo $k \le n$ . O artigo demonstra que estes modelos satisfazem axiomas de teoria de conjuntos padrão (conjunto vazio, separação, união, etc.) nos níveis de truncamento apropriados, desde que os modelos sejam localmente pequenos.
Caracterização dos Tipos de Identidade de M-tipos: O artigo fornece uma caracterização completa do tipo de identidade de M-tipos como M-tipos indexados (Teorema 2.15). Este resultado é usado para provar que os modelos construídos são localmente pequenos, uma condição necessária para que sirvam como modelos válidos de teoria de conjuntos material em HoTT.
Um Modelo do Axioma da Anti-Fundação de Aczel (AFA): Assumindo o axioma de redimensionamento proposicional, os autores constroem um coálgebra terminal para o funtor de conjunto das partes restrito $P^0$ (e, mais genericamente, para funtores baseados em $U$ ). Este coálgebra terminal serve como um modelo do AFA de Aczel, onde cada grafo possui uma decoração única.
Não-Terminalidade de $V^0_\infty$ : O artigo demonstra explicitamente que $V^0_\infty$ não é o coálgebra terminal para $P^0$ . Eles fornecem um contraexemplo mostrando que distintos homomorfismos de coálgebra podem existir de um grafo específico para $V^0_\infty$ , distinguindo-o do coálgebra terminal construído via o método Aczel–Mendler.

Significância e Alegações
O artigo afirma fornecer os primeiros modelos de conjuntos materiais não-bem-fundados em HoTT onde a igualdade é o tipo de identidade, indo além dos modelos baseados em setoids do passado.

Distinção entre AFA e SAFA: O trabalho esclarece a relação entre os axiomas de anti-fundação de Aczel e de Scott dentro do contexto da HoTT. Mostra que, enquanto o coálgebra terminal (que requer redimensionamento proposicional) valida o AFA, o ponto fixo co-iterativo (construtível sem redimensionamento) valida o SAFA. Os autores observam que, no caso não-truncado ( $\infty$ ), AFA e SAFA coincidem, mas divergem em níveis de truncamento inferiores.
Natureza Construtiva: A construção do modelo SAFA ( $V^n_\infty$ ) é totalmente construtiva e não depende de axiomas impredicativos como o redimensionamento proposicional.
Formalização: Todos os principais resultados são formalizados no assistente de prova Agda, utilizando tanto o Agda padrão quanto o Cubical Agda (para a Seção 6), garantindo a correção dos complexos argumentos homotópicos.
Questões Abertas: Os autores notam modestamente que a existência do coálgebra terminal para $P^0$ sem redimensionamento proposicional permanece uma questão aberta. Eles não alegam ter resolvido se tal construção é possível ou se sua existência implica princípios clássicos, mas destacam isso como uma motivação primária para trabalhos futuros.

Em resumo, o artigo expande com sucesso a teoria de conjuntos não-bem-fundados para o cenário de maior dimensão da HoTT, fornecendo modelos distintos para diferentes axiomas de anti-fundação e estabelecendo a base técnica necessária em relação aos M-tipos e estruturas de coálgebra.