Univalence without function extensionality

1. Formulação do Problema

O artigo aborda uma questão fundamental na Teoria dos Tipos de Homotopia (HoTT) relativa à relação lógica entre a Univalência (UA) e a Extensionalidade de Funções (FE).

• Contexto: É um teorema padrão (devido a Voevodsky) que, em qualquer universo univalente, a extensionalidade de funções vale. Ou seja, se duas funções são homotópicas ($f \sim g$), elas são iguais ($f = g$).
• A Questão: O inverso vale? Especificamente, uma forma mais fraca de univalência, que afirma que o universo forma uma "categoria selvagem univalente" (onde a igualdade de tipos corresponde à existência de inversos estritos, isto é, equivalências categóricas), implica a extensionalidade de funções?
• Contexto: François G. Dorais propôs um enfraquecimento chamado Univalência Categórica (CUA), onde o mapa da igualdade de tipos para a equivalência categórica (mapas com inversos esquerdos e direitos estritos) é uma equivalência. Os autores investigam se a CUA implica a FE.

2. Metodologia

Os autores empregam a construção de modelo polinomial de Von Glehn ($Poly(\mathcal{C})$) para construir um contraexemplo. Este método é uma fonte conhecida de modelos para a Teoria dos Tipos de Martin-Löf (ITT) que refutam a extensionalidade de funções.

• Modelo Base ($\mathcal{C}$): Eles começam com um modelo $\mathcal{C}$ de ITT que satisfaz Univalência e Extensionalidade de Funções (por exemplo, um modelo cúbico) e possui coprodutos finitos extensivos satisfazendo regras $\eta$ estritas.
• Construção do Modelo Polinomial: Eles constroem o modelo polinomial $Poly(\mathcal{C})$. Neste modelo:
  • Tipos são pares $(S, P)$ representando "formas" e "posições".
  • A construção está relacionada à interpretação Dialectica de Gödel e à categoria de contentores.
  • Crucialmente, sabe-se que $Poly(\mathcal{C})$ sempre refuta a FE.
• Análise de Isomorfismos: O trabalho técnico central envolve analisar a estrutura de isomorfismos (equivalências categóricas) dentro do modelo polinomial. Os autores decompõem o tipo de isomorfismos entre dois tipos no modelo polinomial em:
  1. Isomorfismos entre seus componentes de "forma" (no modelo base $\mathcal{C}$).
  2. Isomorfismos entre seus componentes de "posição", condicionados ao isomorfismo de forma.

3. Definições e Conceitos Chave

• Categoria Selvagem: Uma estrutura que captura a natureza $(\infty, 1)$-categórica dos tipos, onde composição e identidades satisfazem leis de coerência até a igualdade (não necessariamente homotopia).
• Equivalência Categórica ($A \sim= B$): Um mapa $f: A \to B$ equipado com inversos esquerdos e direitos estritos ($sf = id, fs = id$). Isto difere de uma equivalência homotópica ($A \simeq B$), onde os inversos existem apenas até homotopia.
• Univalência Categórica (CUA): O princípio de que o mapa $(A = B) \to (A \sim= B)$ é uma equivalência.
• Univalência Categórica Familiar (CUA$^\bullet$): Uma variante mais forte que afirma que, para qualquer tipo de índice $I$, a categoria de famílias indexadas por $I$ é univalente no sentido categórico.
• Decomposição da Univalência: O artigo estabelece que a Univalência padrão (UA) é logicamente equivalente à conjunção de Univalência Categórica (CUA) e Extensionalidade de Funções (FE).
  $$UA \iff (CUA \land FE)$$

4. Contribuições e Resultados Chave

A. Independência da CUA e da FE

O resultado primário é a prova de que a Univalência Categórica Familiar não implica a Extensionalidade de Funções.

• Teorema: $ITT + CUA^\bullet_U \nvdash FE_U$.
• Estratégia de Prova:
  1. Tome um modelo base $\mathcal{C}$ satisfazendo $UA + FE$.
  2. Construa $Poly(\mathcal{C})$.
  3. Preservação da CUA: Os autores provam (Teorema 4.17) que, se o modelo base $\mathcal{C}$ satisfaz a Univalência Categórica Familiar, então o modelo polinomial $Poly(\mathcal{C})$ também a satisfaz. Isso depende do fato de que os isomorfismos no modelo polinomial são determinados pelos isomorfismos no modelo base (formas) e por condições específicas nas posições que são contráteis quando o modelo base é univalente.
  4. Refutação da FE: É uma propriedade conhecida dos modelos polinomiais (Proposição 5.3) que eles refutam a Extensionalidade de Funções.
  5. Conclusão: $Poly(\mathcal{C})$ é um modelo de $ITT + CUA^\bullet_U + \neg FE_U$.

B. Hierarquia de Variantes da Univalência

O artigo explora o panorama dos axiomas de univalência enfraquecidos, mostrando que nem todos são equivalentes:

• CUA vs. CUA$^\bullet$: Os autores mostram que a CUA (para um único universo) não implica a Univalência Categórica Familiar (CUA$^\bullet$). Eles constroem um modelo de fatia onde a CUA vale, mas a CUA$^\bullet$ falha.
• Univalência Categórica Categórica (CCUA): Eles definem uma variante onde o mapa $(A=B) \to (A \sim= B)$ é uma equivalência categórica em vez de uma equivalência homotópica. Eles mostram que isto é estritamente mais forte que a CUA, mas ainda não implica a FE.
• Univalência Aproximada: Eles discutem a "univalência aproximada" de Van den Berg (existência de um caminho para cada equivalência) e notam que sua relação com a FE permanece uma questão em aberto, embora modelos polinomiais refutem uma "melhoria de equivalência aproximada" relacionada.

5. Significado

• Desacoplamento de Axiomas: O artigo demonstra que a propriedade de "univalência" de um universo pode ser separada da propriedade de "extensionalidade de funções". Isso desafia a intuição de que a univalência é um axioma monolítico que força todos os princípios de extensionalidade.
• Insight Estrutural: Ao mostrar que a Univalência se fatora em Univalência Categórica e Extensionalidade de Funções, os autores fornecem uma compreensão estrutural mais clara do que faz o axioma da univalência "funcionar". Isso sugere que as funções são "privilegiadas" na declaração padrão da univalência especificamente devido à interação com a FE.
• Teoria de Modelos: O trabalho valida a construção de modelos polinomiais como uma ferramenta poderosa para separar axiomas sutis na teoria dos tipos, estendendo sua utilidade além de apenas refutar a FE para analisar a estrutura interna da univalência.
• Implicações Fundamentais: Para construtivistas e pesquisadores fundamentais, isso sugere que se pode adotar uma forma de univalência (univalência categórica) que preserva a equivalência estrutural dos tipos sem se comprometer com o princípio mais forte, historicamente difícil de integrar, da extensionalidade de funções.

Em resumo, o artigo resolve a questão de Dorais de forma negativa: a Univalência Categórica é estritamente mais fraca que a Univalência completa e não implica a Extensionalidade de Funções.