A type theory for invertibility in weak $ω$-categories

1. O Problema

A teoria das categorias de ordem superior (𝜔-categorias) é fundamental para a teoria da homotopia e para a formalização de estruturas matemáticas complexas. No entanto, a noção de invertibilidade em 𝜔-categorias fracas é sutil e complexa:

• Em categorias ordinárias, um morfismo é invertível se possui um inverso estrito.
• Em bicategorias, a igualdade estrita é substituída por células invertíveis de dimensão superior.
• Em 𝜔-categorias (infinitas), a invertibilidade deve ser entendida coindutivamente. Isso significa que provar que uma célula é invertível exige a produção de uma quantidade infinita de dados (inversos, unitários, associadores, e suas próprias inversibilidades, e assim por diante).

A teoria de tipos existente para 𝜔-categorias fracas, chamada CaTT (introduzida por Finster e Mimram), permite descrever essas estruturas, mas carece de uma maneira interna e sintática para raciocinar sobre a invertibilidade. Sem isso, é difícil formalizar conceitos centrais como equivalências fracas e equifibrações (análogos a isofibrações) diretamente no sistema de tipos, exigindo raciocínio metateórico complexo.

2. Metodologia

Os autores propõem uma extensão conservativa do CaTT chamada ICaTT (Invertible CaTT). A metodologia baseia-se em:

• Extensão Sintática: Adição de um construtor de tipo Inv(A)(t) que testemunha que um termo t possui uma estrutura de invertibilidade.
• Construtores e Destrutores:
  • Destrutores: Permitem extrair dados de invertibilidade (inverso esquerdo, inverso direito, unitários esquerdo e direito, e suas estruturas de invertibilidade recursivas).
  • Construtores:
    • inv: Constrói uma estrutura de invertibilidade a partir de dados explícitos.
    • can (Canônico): Internaliza um teorema que afirma que células de coerência (como composições e identidades) são invertíveis se seus componentes o forem.
    • rec: Um recursor que permite definir estruturas de invertibilidade de forma recursiva, essencial para lidar com a natureza coindutiva infinita sem precisar escrever dados infinitos explicitamente.
• Semântica via Categorias de Modelos: Os autores utilizam a estrutura de clãs (clans) para definir modelos da teoria. Eles mostram que os modelos de ICaTT podem ser interpretados em 𝜔-categorias marcadas (marked 𝜔-categories), onde as células "marcadas" correspondem às células invertíveis.
• Implementação Computacional: Desenvolvimento de um assistente de prova (baseado na implementação existente do CaTT) para verificar as propriedades formalizadas.

3. Principais Contribuições

1. Definição de ICaTT: Uma teoria de tipos dependente que internaliza a invertibilidade coindutiva. Ela adiciona tipos Inv e regras de inferência que permitem construir e deconstruir estruturas de invertibilidade sintaticamente.
2. Conservatividade: Demonstração de que ICaTT é uma extensão conservativa do CaTT. Isso significa que qualquer termo ou tipo válido no CaTT permanece válido em ICaTT, e não há novos teoremas sobre os tipos originais do CaTT que não pudessem ser provados antes. A inclusão entre as categorias sintáticas é fielmente cheia (fully faithful).
3. Formalização da "Walking Equivalence": Os autores mostram que o contexto de ICaTT pode descrever a "walking equivalence" (a equivalência universal), um objeto crucial na caracterização de equifibrações, que não pode ser descrito como um contexto finito no CaTT padrão devido à sua natureza infinita.
4. Semântica em Categorias Marcadas Fibrantes: Construção de uma semântica para ICaTT que mapeia modelos para 𝜔-categorias marcadas fibrantes. Neste modelo, as células marcadas são exatamente aquelas que possuem uma estrutura de invertibilidade.
5. Provas Internas: Uso da implementação para formalizar propriedades fundamentais da invertibilidade (como a propriedade 2-of-6 e o fechamento sob composição) diretamente dentro da teoria, eliminando a necessidade de raciocínio metateórico externo.

4. Resultados Chave

• Normalização: Embora o sistema de reescrita de ICaTT não termine (devido à natureza coindutiva e à expansão $\eta$ infinita), os autores provam que o sistema é normalizante para tipos e termos categóricos (aqueles que não envolvem explicitamente construtores de invertibilidade complexos). Isso garante que a teoria é bem-comportada para a maioria das aplicações práticas.
• Caracterização de Equifibrações: A teoria permite caracterizar as equifibrações como morfismos que possuem a propriedade de levantamento à direita contra uma família específica de morfismos derivados da "walking equivalence".
• Propriedade 2-of-6: A formalização bem-sucedida da propriedade 2-of-6 para células invertíveis (se $f \circ g$ e $g \circ h$ são invertíveis, então $f, g, h$ também são) dentro do sistema de tipos.
• Relação com Modelos Existentes: A teoria conecta-se com trabalhos anteriores de Ozornova e Rovelli (sobre a walking equivalence) e Fujii et al. (sobre equifibrações), fornecendo uma base sintática unificada para esses conceitos.

5. Significância e Impacto

• Avanço na Teoria da Homotopia Direcionada: O trabalho fornece uma ferramenta sintática poderosa para trabalhar com equivalências fracas em contextos direcionados, um passo crucial para a construção de uma estrutura de modelo (model structure) para 𝜔-categorias fracas, um problema em aberto na área.
• Ferramenta Prática: A implementação do ICaTT permite que pesquisadores verifiquem propriedades complexas de invertibilidade com esforço mínimo, servindo como um banco de prova para conjecturas sobre a estrutura de 𝜔-categorias.
• Ponte entre Sintaxe e Semântica: Ao construir uma semântica em categorias marcadas fibrantes, o artigo valida a abordagem sintática, mostrando que a teoria de tipos captura corretamente as propriedades homotópicas esperadas das células invertíveis.
• Fundamento para Futuras Estruturas de Modelo: A capacidade de definir e manipular invertibilidade internamente é vista como um pré-requisito essencial para definir cofibrações e equivalências fracas de forma rigorosa, potencialmente levando à resolução do problema da estrutura de modelo para 𝜔-categorias fracas.

Em resumo, o artigo apresenta uma extensão teórica e prática robusta que preenche uma lacuna fundamental na formalização de 𝜔-categorias, permitindo o tratamento sintático direto da invertibilidade coindutiva e abrindo caminho para avanços significativos na teoria da homotopia de ordem superior.