The internal languages of univalent categories

Resumo Técnico: As Linguagens Internas de Categorias Univalentes

Enunciado do Problema
Os teoremas de linguagem interna em lógica categórica estabelecem uma equivalência entre sintaxe (teorias de tipos) e semântica (modelos categóricos). Um resultado seminal de Clairambault e Dybjer [CD14] corrigiu o teorema original de Seely [See84], estabelecendo uma biequivalência entre a bicategoria de categorias localmente cartesianas fechadas (LCCCs) e a bicategoria de categorias democráticas com famílias (CwFs) que suportam tipos de identidade extensional, tipos $\Sigma$ e tipos $\Pi$.

No entanto, este resultado foi formulado dentro de fundações teóricas baseadas em conjuntos. Na fundação univalente (Teoria de Tipos Homotópica), a noção padrão de CwF encontra um obstáculo fundamental: o axioma da univalência implica que o tipo dos conjuntos não é um conjunto em si mesmo (é um 1-tipo). Consequentemente, o requisito em CwFs de que a coleção de tipos em um contexto forme um conjunto é violado pela categoria univalente de conjuntos. Além disso, a distinção entre estrutura "escolhida" (ex: fibrações divididas/split) e estrutura "existente" (ex: limites até isomorfismo) cria problemas de coerência em fundações baseadas em conjuntos que necessitam do axioma da escolha ou de procedimentos de estritificação. Nas fundações univalentes, onde o isomorfismo implica identidade, essas distinções evaporam, mas a estrutura existente de CwFs não é diretamente aplicável.

Metodologia
O artigo desenvolve um novo framework para semântica categórica dentro de fundações univalentes, utilizando categorias univalentes e categorias de compreensão em vez de CwFs.

1. Categorias Univalentes: O autor trabalha com categorias onde o tipo de identidade dos objetos é equivalente ao tipo de isomorfismos (equivalências adjuntas). Isso permite o tratamento de equivalências adjuntas como identidades, simplificando provas sobre a preservação de estrutura (ex: exponenciais) e eliminando a necessidade do axioma da escolha para selecionar limites.
2. Categorias de Compreensão: Para modelar tipos dependentes sem exigir que os tipos formem um conjunto, o artigo adota categorias de compreensão (baseadas em fibrações e categorias exibidas). Uma categoria de compreensão consiste em uma categoria base de contextos, uma categoria exibida de tipos, um cleaving (fornecendo substituição) e um funtor de compreensão. O autor restringe sua atenção a categorias de compreensão totais univalentes, onde tanto a base quanto a categoria exibida são univalentes.
3. Bicatégorias Exibidas: A construção das bicatégorias de modelos baseia-se fortemente em bicatégorias exibidas [AFM+21]. Esta abordagem modular permite que o autor construa bicatégorias complexas (como as de LCCCs ou toposes com universos) sobrepondo propriedades (ex: limites finitos, tipos $\Pi$, universos) sobre bicatégorias de base mais simples. Esta modularidade facilita a prova de que as bicatégorias resultantes são, elas mesmas, univalentes.
4. Propriedades Locais: Para estender resultados de categorias com limites finitos para estruturas mais complexas como toposes, o artigo adapta a noção de propriedades locais de Maietti [Mai05]. Uma propriedade local é uma condição em categorias fechada sob fatiamento (slicing). O autor formaliza isso dentro do framework de bicatégoria exibida para estender biequivalências do caso base (limites finitos) para várias classes de toposes.
5. Reindexação e Universos: Para o tratamento de universos, o artigo emprega a reindexação de bicatégorias exibidas. Esta técnica permite a transferência de uma biequivalência de uma categoria base para uma categoria exibida sobre ela, permitindo a definição de universos fechados sob formadores de tipos específicos (ex: $\Sigma$, $\Pi$, números naturais), não apenas exigindo leis de estabilidade estritas, mas sim estabilidade até isomorfismo (que se torna identidade em categorias univalentes).

Principais Contribuições
O artigo apresenta quatro contribuições primárias:

1. Análogo Univalente de Clairambault-Dybjer: O autor constrói uma biequivalência entre a bicategoria de categorias univalentes com limites finitos e a bicategoria de categorias de compreensão DFL (Finite Limit) totais univalentes. Isso estabelece que a linguagem interna das categorias univalentes com limites finitos é a teoria de tipos de Martin-Löf extensional com unidade, produto binário e tipos $\Sigma$.
2. Extensão para Categorias Localmente Cartesianas Fechadas: A biequivalência é estendida para categorias localmente cartesianas fechadas univalentes e categorias de compreensão DFL que suportam tipos $\Pi$. Isso confirma que a linguagem interna das LCCCs univalentes é a teoria de tipos de Martin-Löf extensional com tipos $\Pi$.
3. Extensão para Toposes e Universos: O método é generalizado para várias classes de toposes (pretoposes, $\Pi$-pretoposes, toposes elementares e toposes com um objeto de números naturais) usando propriedades locais. Além disso, o autor define universos nessas categorias que são fechados sob formadores de tipos (números naturais, classificador de subobjetos, redimensionamento proposicional, tipos $\Sigma$ e tipos $\Pi$), estabelecendo uma biequivalência para toposes elementares com um universo.
4. Formalização: Todas as construções e provas são formalizadas no assistente de prova Rocq utilizando a biblioteca UniMath, garantindo a correção e fornecendo uma referência verificada por máquina para a teoria.

Resultados
O artigo prova que, para várias classes de categorias univalentes, existe uma biequivalência com classes correspondentes de categorias de compreensão univalentes. Especificamente:

• Limites Finitos: Categorias univalentes com limites finitos $\simeq$ categorias de compreensão DFL (Unidade, Produto, Igualador, $\Sigma$).
• LCCC: LCCCs univalentes $\simeq$ categorias de compreensão DFL com tipos $\Pi$.
• Toposes: Toposes elementares univalentes (com/sem NNO) $\simeq$ categorias de compreensão DFL com propriedades locais correspondentes (ex: classificadores de subobjetos, somas disjuntas, quocientes).
• Universos: Toposes elementares univalentes com um universo fechado sob formadores de tipos específicos $\simeq$ categorias de compreensão DFL com um objeto de universo satisfazendo as condições de fechamento correspondentes.

O artigo demonstra que, em fundações univalentes, a linguagem interna dessas estruturas categóricas é a teoria de tipos de Martin-Löf extensional. O uso de categorias univalentes simplifica a teoria ao remover a necessidade de fibrações divididas e do axioma da escolha, que são necessários em fundações baseadas em conjuntos para garantir a correção (soundness). Os problemas de coerência que assolam modelos teóricos de conjuntos (onde a substituição deve ser estrita) são resolvidos porque isomorfismos são identidades.

Significado e Alegações
O artigo afirma que seu desenvolvimento fornece uma nova perspectiva sobre a semântica da teoria de tipos dependentes. Ao utilizar categorias univalentes, o autor evita o overhead técnico de fibrações divididas e do axioma da escolha, que são necessários em fundações baseadas em conjuntos para garantir a correção. O princípio de identidade de estrutura inerente às fundações univalentes permite um tratamento mais natural de estruturas categóricas onde objetos são identificados por equivalência em vez de igualdade estrita.

O autor declara explicitamente que não constrói a sintaxe ou o modelo inicial neste trabalho; em vez disso, foca no lado categórico do teorema da linguagem interna (a equivalência entre modelos). Ele observa que, embora as categorias de compreensão sejam adequadas para fundações univalentes, outras estruturas como CwFs não são, devido à restrição de conjunto sobre os tipos. O artigo posiciona-se como um passo fundamental, deixando o desenvolvimento de uma sintaxe adequada (como a sintaxe de grupoide) e sua interpretação como trabalhos futuros. O significado reside em estabelecer uma correspondência robusta e verificada por máquina entre estruturas categóricas univalentes e teorias de tipos, demonstrando que as fundações univalentes suportam naturalmente esses teoremas de linguagem interna sem os defeitos encontrados em formulações anteriores baseadas em conjuntos.