Extension Types for Free

Resumo Técnico: Tipos de Extensão "De Graça": Cofibrações, Colagem e Univalência em Teoria de Tipos de Dois Níveis

Enunciado do Problema
Tipos de extensão são um conceito fundamental na teoria de tipos dependentes, aparecendo em vários contextos, como teorias de tipos cubicais (caminhos com extremidades fixas), a teoria de tipos simpliciais de Riehl e Shulman (termos fixos em subformas) ou mecanismos de desdobramento controlado. Nos frameworks existentes, esses tipos são tipicamente postulados como novos primitivos, governados por um "cálculo de faces" meta-teórico ou uma camada de forma que dita sua formação e regras. Essa abordagem frequentemente requer construções de modelos específicas ou adições axiomáticas para validar as regras (como condições de contorno estritas, extensionalidade de função relativa e a propriedade de extensão de homotopia). Um problema central aberto na teoria de tipos homotópicos (HoTT) é determinar a relação precisa entre o "book HoTT" (a formulação axiomática do HoTT Book) e as teorias de tipos cubicais, particularmente se são extensões conservativas umas das outras.

Metodologia
O artigo utiliza a Teoria de Tipos de Dois Níveis (2LTT) como um framework unificador. A 2LTT enriquece a HoTT com um nível "estrito" (externo) de igualdade que satisfaz a Unicidade de Provas de Identidade (UIP) e a extensionalidade de função, enquanto o nível "interno" (fibrante) retém a estrutura homotópica padrão.

• Semântica: O framework é semanticamente "livre"; modelos padrão de HoTT (ex: conjuntos simpliciais, conjuntos cubicais) geram automaticamente modelos de 2LTT via construções de presheaves. A teoria é conservativa sobre seu nível interno, o que significa que nenhum novo teorema é provável em sua linguagem interna que não fosse já provável em HoTT.
• Definição de Tipos de Extensão: Em vez de postular tipos de extensão, o artigo os define internamente dentro da 2LTT. Dada uma cofibração $i: \Phi \hookrightarrow \Psi$ (um mapa no nível externo), uma família fibrante $A$ sobre $\Psi$, e uma seção parcial $a$, o tipo de extensão é definido como a fibra estrita do mapa de restrição sobre $a$:
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  Aqui, $=_s$ denota a igualdade estrita do nível externo.
• Cofibrações: O "cálculo de faces" é substituído pela classe de cofibrações no nível externo. O artigo trata a escolha específica de quais mapas são cofibrações como um parâmetro, permitindo que o framework se adapte a diferentes configurações (simplicial, cubical, etc.) sem alterar a definição central.

Contribuições Principais e Resultados

1. Tipos de Extensão "De Graça":
   O artigo demonstra que, na 2LTT, todo o cálculo de tipos de extensão proposto por Riehl e Shulman é definível em vez de axiomático.

• Regras Estritas: As regras de introdução, eliminação, $\beta$, $\eta$ e de contorno (boundary) são válidas estritamente por construção.
• Axiomas Prováveis: Axiomas que são postulados em outros contextos, como a extensionalidade de função relativa e a propriedade de extensão de homotopia (realinhamento), tornam-se teoremas derivados das propriedades de cofibrações e fibrações na 2LPT.
• Unificação: Esta definição única subsume várias instâncias existentes, incluindo caminhos cubicais, tipos de extensão de Riehl-Shulman e tipos indexados por proposições (desdobramento controlado).

2. Equivalência de Colagem (Gluing) e Univalência:
   O artigo estabelece um ciclo preciso de implicações conectando a colagem cubical e o axioma de univalência dentro do framework 2LTT:

• Univalência $\implies$ Colagem: Se o universo interno for univalente, então, para qualquer cofibração, o tipo dos "dados de Glue" (estruturas necessárias para formar um tipo Glue) é contratável. Isso implica a existência de uma estrutura Glue que satisfaz as regras em forma homotópica.
• Colagem $\implies$ Univalência: Inversamente, a existência de uma "estrutura de Glue fraca" (que requer apenas igualdades internas para concordância de contorno e uma estrutura de intervalo de caminho) implica que o universo é univalente.
• Resultado: Na presença de um intervalo de caminho, univalência e a existência de dados de Glue contratáveis são equivalentes. Isso inverte a direção padrão de implicação (que a existência de tipos Glue implica Univalência) e estabelece uma equivalência de mão dupla.

3. Formalização:
   Todos os resultados da Seção 2 até a Seção 5 são auto-formalizados em Agda utilizando a flag --two-level. A formalização combina argumentos de HoTT internos com raciocínio externo sobre o nível estrito, verificando a consistência e correção das afirmações teóricas.

4. Abordagem à Conservatividade:
   O artigo propõe uma estratégia para abordar o problema aberto de saber se as teorias de tipos cubicais são conservativas sobre o book HoTT. Ao representar ambas as teorias dentro da 2LTT:

• O Book HoTT é representado como MLTT + Univalência (nível interno).
• A Teoria de Tipos Cubicais é representada como MLTT + Glue + Intervalo de Caminho (suposições estruturais/externas).
• O artigo prova que, sobre uma teoria base com um intervalo de caminho, o axioma de Univalência e o axioma de Glue são inter-deriváveis. Isso sugere que a diferença central entre as teorias pode ser estrutural em vez de lógica, oferecendo uma rota para provar a conservatividade.

Significância e Alegações
O artigo afirma que o framework da 2LTT fornece uma fundação "gratuita" e uniforme para tipos de extensão, removendo a necessidade de axiomas ad-hoc ou construções de modelos específicos para validar suas regras. Ao internalizar o cálculo de faces como cofibrações, a teoria unifica ocorrências díspares de tipos de extensão encontradas na literatura.

Em relação à conexão entre teorias de tipos cubicais e o book HoTT, o artigo é modesto. Ele não afirma ter resolvido a conjectura de conservatividade. Em vez disso, oferece uma prova de conceito: demonstra que o mecanismo central da teoria de tipos cubicais (colagem/gluing) é logicamente equivalente ao axioma central da HoTT (univalência) quando visto através da lente da 2LTT. Essa equivalência permite que pesquisadores traduzam extensões estruturais (como tipos Glue) em extensões axiomáticas dentro de um único framework, facilitando a comparação e potencialmente pavimentando o caminho para futuras provas de conservatividade. O artigo observa explicitamente que a suposição de um "intervalo de caminho" no lado da HoTT permanece um desafio aberto para estabelecer uma equivalência total.