Univalent Enriched Categories and the Enriched Rezk Completion

Resumo Técnico: Categorias Enriquecidas Univalentes e a Conclusão de Rezk Enriquecida

Enunciado do Problema
A teoria das categorias é um arcabouço fundamental para a matemática e a ciência da computação, com categorias enriquecidas desempenhando um papel crítico na teoria das categorias superiores, na teoria da homotopia e na semântica de linguagens de programação (por exemplo, usando DCPOs para linguagens com efeitos). No entanto, no contexto das Fundações Univalentes (Teoria dos Tipos Homotópicos), a definição padrão de categorias frequentemente falha em satisfazer o princípio da equivalência, que estabelece que objetos isomórficos devem ser indistinguíveis. Embora "categorias univalentes" (onde a identidade de objetos é equivalente ao isomorfismo) tenham sido estabelecidas para categorias ordinárias, a teoria das categorias enriquecidas univalentes permanece subdesenvolvida. Especificamente, há uma falta de resultados formalizados em relação ao princípio da identidade de estrutura, à caracterização de equivalências e à existência de uma conclusão de Rezk (uma reflexão univalente) para categorias enriquecidas. Além disso, construções padrão como categorias de Kleisli frequentemente falham em ser univalentes, necessitando de um método para construir análogos univalentes no cenário enriquecido.

Metodologia
O artigo desenvolve a teoria de categorias enriquecidas dentro do assistente de provas Rocq utilizando a biblioteca UniMath, aderindo às Fundações Univalentes. A abordagem metodológica central envolve:

1. Enriquecimentos como Estrutura: Em vez de definir categorias enriquecidas como uma coleção de objetos e objetos-hom (a definição de Kelly), os autores as definem como uma categoria juntamente com um enriquecimento. Um enriquecimento consiste em objetos-hom em uma categoria monoidal, morfismos de identidade e composição, e uma correspondência entre morfismos na categoria subjacente e elementos dos objetos-hom. Essa perspectiva trata uma categoria enriquecida como uma categoria univalente dotada de estrutura extra.
2. Bicatégorias Exibidas: Para provar o princípio da identidade de estrutura, os autores utilizam a maquinaria de bicatégorias exibidas (displayed bicategories). Eles definem uma bicatégoria exibida $dEnrichCat_{\mathcal{V}}$ sobre a bicatégoria de categorias univalentes ($UnivCat$). A bicatégoria total deste exibimento é $EnrichCat_{\mathcal{V}}$. Isso permite o reuso de resultados de univalência existentes para $UnivCat$ para provar a univalência para o cenário enriquecido.
3. Sistemas de Fatoração Ortogonal: Para caracterizar equivalências, o artigo emprega sistemas de fatoração ortogonal em bicatégorias. Ele define funtores enriquecidos totalmente fiéis e essencialmente sobrejetivos e prova que eles formam um sistema de fatoração ortogonal.
4. Duas Construções da Conclusão de Rezk: O artigo fornece duas construções distintas para a conclusão de Rezk de uma categoria enriquecida:
   • Imersão de Yoneda: Construindo a conclusão como a imagem da imersão de Yoneda enriquecida. Isso requer que $\mathcal{V}$ seja completa e simétrica monoidal fechada, mas baseia-se na teoria de categorias padrão.
   • Tipos Indutivos Superiores (HITs): Construindo a conclusão dotando a conclusão de Rezk da categoria subjacente com um enriquecimento usando as regras de eliminação de HITs. Esta abordagem evita suposições de completude ou fechamento de $\mathcal{V}$ e preserva os níveis de universo se o universo for fechado sob HITs.
5. Propriedades Universais: O artigo estabelece a propriedade universal da conclusão de Rezk, demonstrando que a pré-composição com uma equivalência fraca (functor totalmente fiel e essencialmente sobrejetivo) induz uma equivalência adjunta entre categorias de funtores.

Principais Contribuições e Resultados

• Princípio da Identidade de Estrutura: O artigo prova que a bicatégoria de categorias enriquecidas univalentes ($EnrichCat_{\mathcal{V}}$) é univalente (Teorema 2.8). Isso implica que o tipo de identidade entre duas categorias enriquecidas univalentes é equivalente ao tipo de equivalências adjuntas entre elas.
• Caracterização de Equivalências: Prova-se que todo funtor enriquecido que é tanto totalmente fiel quanto essencialmente sobrejetivo é uma equivalência adjunta (Teorema 4.8). Este resultado é construtivo e baseia-se no fato de o domínio e o codomínio serem univalentes, evitando o axioma da escolha.
• Conclusão de Rezk: Duas construções para a conclusão de Rezk de categorias enriquecidas são fornecidas (Construções 5.5 e 5.7). O artigo prova que toda categoria enriquecida admite uma conclusão de Rezk e satisfaz a propriedade universal de que qualquer funtor para uma categoria univalente se estende unicamente ao longo de equivalências fracas (Teorema 5.2).
• Categorias de Kleisli Univalentes: Os autores constroem categorias de Kleisli enriquecidas univalentes. Eles definem a categoria de Kleisli padrão $K(T)$ e seu contraparte univalente $Kleisli(T)$ (como uma subcategoria plena da categoria de Eilenberg-Moore). Usando a conclusão de Rezk e a propriedade universal, eles mostram que $Kleisli(T)$ satisfaz a propriedade universal de objetos de Kleisli na bicatégoria de categorias enriquecidas univalentes (Construção 6.9).
• Exemplos e Caracterizações: O artigo fornece inúmeros exemplos, incluindo auto-enriquecimento, enriquecimentos opostos e mudanças de base. Ele caracteriza enriquecimentos sobre estruturas cartesianas (como DCPOs) e introduz uma noção de "estrutura fechada suportando produtos smash" para lidar com conjuntos pontuados e ordinais, embora note limitações em relação a DCPOs pontuados.

Significância e Alegações
O artigo afirma estabelecer uma fundação robusta para a teoria de categorias enriquecidas dentro das Fundações Univalentes. Sua principal significância reside em:

1. Formalização: Fornecer uma biblioteca formalizada em Rocq/UniMath para categorias enriquecidas, que anteriormente carecia de formalização extensa em comparação com categorias ordinárias.
2. Correção da Noção: Demonstrar que visualizar categorias enriquecidas como categorias univalentes com estrutura extra (via enriquecimentos) simplifica as provas de propriedades fundamentais como o princípio da identidade de estrutura.
3. Resolução da Não-Univalência: Abordar a questão de que construções comuns (como categorias de Kleisli) não são inerentemente univalentes, fornecendo um método sistemático (conclusão de Rezk) para obter versões univalentes que preservam as propriedades universais necessárias.
4. Ferramentas Fundacionais: Estabelecer a bicatégoria de categorias enriquecidas univalentes como uma bicatégoria univalente, o que é um pré-requisito para o desenvolvimento de uma teoria de categorias interna posterior (ex: monads, limites) em um ambiente univalente.

Os autores observam que, embora sua abordagem cubra muitos casos padrão, ela possui limitações em relação aos produtos smash para certas estruturas (como DCPOs pontuados) onde os quocientes devem ser tomados na categoria apropriada em vez de conjuntos. Eles sugerem que trabalhos futuros poderiam envolver o desenvolvimento do equipamento de categorias enriquecidas ou a generalização da noção de produto smash para lidar com esses casos.