A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism

1. Problema e Contexto

O artigo aborda a necessidade de uma caracterização abstrata e unificada de teorias de tipos, especificamente aquelas que envolvem polimorfismo de universos explícito.

• O Desafio: As definições tradicionais de teorias de tipos baseiam-se em gramáticas e regras de inferência sintáticas. Isso introduz uma complexidade desnecessária devido a escolhas sintáticas arbitrárias e regras de "contabilidade" (como regras de igualdade geral), dificultando a prova de propriedades metateóricas e a comparação entre diferentes formalismos.
• O Projeto de Voevodsky: O trabalho se insere no contexto da "Conjectura de Inicialidade" proposta por Vladimir Voevodsky. O objetivo é definir uma classe geral de teorias de tipos dependentes e provar que o modelo de termos (a sintaxe) é um objeto inicial na categoria de modelos. Isso permitiria obter resultados semânticos para novas teorias de tipos através da especialização de teoremas gerais, em vez de reconstruir provas para cada sistema.
• Polimorfismo de Universos: O foco específico está em teorias onde os níveis de universo não são apenas uma hierarquia externa fixa, mas onde os níveis são tratados como termos de primeira classe (com julgamentos de nível explícitos) e onde existem produtos indexados por níveis.

2. Metodologia

Os autores utilizam uma abordagem baseada em Teorias Algébricas Generalizadas (GATs - Generalized Algebraic Theories) e Categorias com Famílias (CwFs - Categories with Families).

• Abordagem Categorical: Em vez de definir a teoria por regras de inferência, eles a definem como uma GAT. Uma GAT generaliza teorias algébricas multissortadas permitindo que os símbolos de sort e operadores tenham tipos dependentes.
• CwFs como Modelos: As Categorias com Famílias são usadas como a estrutura semântica padrão para teorias de tipos dependentes. Um modelo de uma GAT é um CwF com estrutura extra que satisfaz certas equações.
• Construção de Modelos Iniciais: O artigo explora a construção de modelos iniciais para essas GATs. Um modelo inicial representa a "sintaxe livre" da teoria. Se a teoria é capturada por uma GAT, a existência de um modelo inicial é garantida (ou construída), e a sintaxe da teoria de tipos é isomorfa a este modelo inicial.
• Duas Variações Analisadas:
  1. Torre Externa de Universos: Uma versão onde os universos são indexados por números naturais externos ($l \in \mathbb{N}$).
  2. Polimorfismo Explícito (Interno): Uma versão onde os níveis de universo são termos internos, com julgamentos de igualdade de níveis e produtos indexados por níveis.

3. Contribuições Principais

O artigo apresenta duas GATs específicas e suas correspondentes construções de modelos iniciais:

A. GAT para Teoria de Tipos com Torre Externa de Universos ($\Sigma_{tower}$)

• Estrutura: Uma GAT infinitária baseada em CwFs com estrutura extra para os formadores de tipos pequenos ($\Pi, \Sigma, N_0, N_1, N, W, Id$) e uma torre de universos $U_l$ indexada por $l \in \mathbb{N}$.
• Operadores: Inclui operadores para a formação de universos, mapas de decodificação ($T_l$), e códigos para tipos dentro dos universos.
• Resultado: Demonstra-se que a teoria de tipos com torre externa pode ser caracterizada como o modelo inicial desta GAT. O artigo discute como construir este modelo inicial como uma união de modelos finitários (torres truncadas).

B. GAT para Teoria de Tipos com Polimorfismo de Universos Explícito ($\Sigma_{up}$)

• Inovação: Esta é a contribuição central. A teoria lida com níveis de universo como objetos internos.
• CwF Indexado por Níveis: A estrutura base não é um único CwF, mas um CwF indexado por um CwF unificado de níveis (ucwf).
  • Existe um "CwF de Níveis" ($L$) que trata contextos de níveis, substituições de níveis e termos de níveis.
  • Existe um CwF de tipos pequenos indexado por $L$ ($T: L^{op} \to CwF$).
• Igualdade de Níveis: Introduz-se um símbolo de sort especial leq para igualdade proposicional de níveis. Isso permite expressar restrições como $l < m$ (definida como $l^+ \lor m = m$) dentro da própria teoria, sem depender de premissas externas.
• Produtos Indexados por Níveis: Inclui operadores para quantificação universal de nível ($[\alpha]A$), abstração de nível e aplicação de nível.
• Polimorfismo e Cumulatividade: A GAT suporta tanto a versão não cumulativa quanto a cumulativa (onde um universo é um subconjunto de um universo maior), com operadores de elevação ($T^m_l$) e equações correspondentes.

4. Resultados Técnicos

1. Caracterização Abstrata: As teorias de tipos (com torre externa e com polimorfismo explícito) são rigorosamente caracterizadas como os modelos iniciais das respectivas GATs ($\Sigma_{tower}$ e $\Sigma_{up}$).
2. Construção de Modelos Iniciais:
   • Para $\Sigma_{tower}$ (infinitária), o modelo inicial é construído como o limite de uma sequência de modelos finitários.
   • Para $\Sigma_{up}$ (finitária), o modelo inicial é construído diretamente, garantindo a existência de um objeto inicial na categoria de CwFs com estrutura $\Sigma_{up}$.
3. Equivalência de Abordagens: O artigo esboça como construir o modelo inicial tanto a partir de uma sintaxe com substituição explícita (usando a construção genérica de GATs) quanto a partir de uma sintaxe com substituição implícita (a sintaxe usual de teorias de tipos), mostrando que ambas levam ao mesmo objeto inicial (até isomorfismo).
4. Generalização: A abordagem demonstra que sistemas lógicos diversos (lógica de predicados, lógica não tipada) podem ser capturados como variações de CwFs indexados e formalizados como GATs.

5. Significado e Impacto

• Avanço na Conjectura de Inicialidade: O trabalho fornece uma implementação concreta e uma prova de conceito para o projeto de Voevodsky. Ao caracterizar teorias de tipos complexas (com polimorfismo de universos) como modelos iniciais de GATs, os autores fornecem um caminho rigoroso para provar que a sintaxe é o objeto inicial na categoria de modelos.
• Abstração de Detalhes Sintáticos: Ao elevar o nível de abstração para GATs, o trabalho permite ignorar detalhes de implementação (como a escolha entre substituição explícita ou implícita, ou regras de igualdade específicas) e focar na estrutura categórica essencial da teoria.
• Unificação de Lógica e Teoria de Tipos: A abordagem reforça a visão de que a lógica e a teoria de tipos podem ser tratadas uniformemente através de estruturas algébricas generalizadas, conectando-se a trabalhos anteriores de Lawvere e Cartmell.
• Base para Futuras Extensões: A introdução do sort de igualdade de níveis (leq) abre caminho para formalizar restrições equacionais complexas dentro da própria estrutura da teoria, o que é crucial para o desenvolvimento de fundamentos univalentes e sistemas de tipos mais expressivos.

Em resumo, o artigo oferece uma fundação categórica robusta para teorias de tipos com polimorfismo de universos explícito, transformando a sintaxe complexa em um objeto matemático bem-definido (o modelo inicial de uma GAT), facilitando assim a verificação de propriedades e a comparação entre diferentes sistemas de tipos.