Directed type theory, with a twist

1. Problema e Motivação

A Teoria de Homotopia de Tipos (HoTT) estabeleceu-se com grande sucesso como uma fundação para a matemática e como uma linguagem sintética para raciocinar sobre $\infty$-grupos (espaços). No entanto, em muitas áreas da matemática e da ciência da computação, as categorias (e não apenas os grupos) são as estruturas fundamentais a serem consideradas.

Várias teorias de tipos direcionadas foram propostas para endereçar isso, buscando fornecer uma linguagem interna para categorias. Contudo, trabalhos anteriores (como os de Licata & Harper, North, e Riehl & Shulman) falharam em satisfazer simultaneamente três desideratos (objetivos de design) cruciais para uma teoria robusta:

1. Tipos como Categorias: Todo tipo no contexto vazio deve semanticamente corresponder a uma categoria (evitando que tipos sejam estruturas mais gerais das quais as categorias são apenas um subconjunto restrito).
2. Estrutura Categórica Emergente: A teoria deve possuir tipos de Hom (direcionados) definidos por regras de formação, introdução, eliminação e computação, permitindo codificar células $n$-dimensionais como iterações do tipo Hom.
3. Igualdades Direcionadas Triviais via Objetos de Caminho: A regra de introdução do tipo Hom deve corresponder à fatoração do mapa diagonal através da categoria de setas ($A^\to$), permitindo o raciocínio sobre transformações naturais de forma análoga às homotopias na HoTT.

O trabalho anterior de North satisfazia os dois primeiros, mas falhava no terceiro, pois a regra de introdução do Hom estava restrita ao núcleo de grupoide, não capturando a estrutura completa da categoria de setas.

2. Metodologia e Abordagem

Os autores, Fernando Chu e Paige Randall North, propõem a Teoria de Tipos Twistada (Twisted Type Theory - TTT). A metodologia baseia-se em:

• Modelo Semântico: Utilizam o "modelo de categorias" de North, onde contextos são interpretados como categorias e tipos como categorias indexadas.
• Novo Operador "Twist" (Torção): Introduzem uma operação sintática e semântica inovadora. Dado um tipo que depende tanto contravariantemente quanto covariantemente de certas variáveis, o "twist" produz um novo tipo que depende apenas covariantemente dessas mesmas variáveis.
• Generalização de Fibras: Para dar semântica a essa operação, introduzem o conceito de Fibras 2-Laterais Dependentes (Dependent 2-Sided Fibrations - D2SFibs). Isso generaliza a noção clássica de Street de fibras 2-laterais para o caso dependente.
• Teorema de Straightening-Unstraightening: Estabelecem um teorema que caracteriza as D2SFibs, mostrando uma equivalência entre profunctors dependentes e essas fibras. O "twist" de um tipo corresponde semanticamente à parte "unstraightening" (desendireitamento) dessa caracterização.
• Regras Modificadas para Hom: Reformulam as regras de introdução e eliminação para tipos Hom, utilizando o operador twist para garantir que a interpretação do tipo Hom introduza corretamente a categoria de setas ($A^\to$).

3. Contribuições Principais

1. Definição da TTT: Uma extensão da Teoria de Tipos de Martin-Löf (MLTT) que incorpora tipos twistados, tipos Hom modificados, tipos opostos, universos discretos e contextos opostos.
2. Operador Twist e D2SFibs: A introdução formal da operação de twist e o desenvolvimento da teoria das Fibras 2-Laterais Dependentes, incluindo o teorema de straightening-unstraightening para o caso dependente.
3. Regra de Introdução do Hom (Hom-Intro): Uma regra sintática análoga à regra de introdução de identidade ($refl$) na HoTT, mas para tipos direcionados. Semanticamente, ela mapeia um elemento $a$ para a identidade $id_a$ na categoria de setas, satisfazendo o desiderato de que a categoria de setas seja recuperada corretamente.
4. Regra de Eliminação do Hom (Hom-Elim): Uma regra de eliminação que permite raciocinar sobre transformações naturais. Ela é formulada de modo que o "motive" (motivo) da eliminação possa depender de uma variável adicional, superando a limitação de que produtos dependentes de op-fibras nem sempre são op-fibras.
5. Conexão com Estruturas Existentes: Demonstram como o twist se relaciona com tipos $\Sigma$, tipos $\Pi$ e limites lax (lax ends), unificando conceitos dispersos na literatura de tipos direcionados.

4. Resultados Chave

• Validação do Modelo: O modelo de categorias valida todas as regras propostas, incluindo a nova regra de introdução e eliminação do Hom.
• Unicidade Direcionada (Directed Univalence): Para conjuntos (tipos discretos), a teoria valida a equivalência entre o tipo de funções $A \to B$ e o tipo Hom $Hom_{Set}(A, B)$, generalizando a univalência para o caso direcionado.
• Transformações Naturais Sintéticas: A teoria permite representar transformações naturais sinteticamente. Termos do tipo twistado $Hom(Fa, Ga)$ correspondem diretamente a transformações naturais entre funtores no modelo semântico.
• Prova Sintética do Lema de Yoneda: Os autores utilizam a TTT para fornecer uma prova sintética do Lema de Yoneda. A prova demonstra que o isomorfismo entre o functor de Yoneda e a avaliação pode ser construído diretamente usando as regras de eliminação do Hom, sem necessidade de argumentos semânticos externos complexos.
• Extensão de Funções (Function Extensionality Direcionada): Estabelecem um axioma de extensão de função direcionada, permitindo que transformações naturais entre funtores sejam tratadas como igualdades em certos contextos (especificamente para copresheaves em Set).

5. Significado e Impacto

A TTT representa um avanço significativo na formalização de teoria de categorias dentro da teoria de tipos dependentes:

• Fundação Matemática: Oferece uma base mais sólida para a matemática direcionada, onde a igualdade é não-simétrica (morfismos), permitindo tratar categorias como objetos de primeira classe, e não apenas como estruturas derivadas.
• Simplicidade Semântica vs. Poder Sintético: Ao focar no modelo de categorias (em vez de modelos de $\infty$-categorias), os autores conseguem manter a complexidade semântica gerenciável enquanto replicam as técnicas de prova da HoTT (como eliminação de identidade/Hom).
• Ponte entre Sintaxe e Semântica: A introdução do "twist" resolve um problema histórico em teorias direcionadas: como obter a categoria de setas a partir de tipos dependentes. Isso permite que a sintaxe "veja" a estrutura de setas de forma natural.
• Futuro: O trabalho abre caminho para o desenvolvimento de modelos de dimensão superior (análogos à HoTT para categorias) e para a exploração de estruturas de fatoração fraca generalizadas (D2SFibs) que podem refinar ainda mais os princípios de eliminação.

Em resumo, a TTT preenche lacunas críticas em teorias de tipos direcionados anteriores, fornecendo uma ferramenta poderosa para raciocínio sintético sobre categorias, com aplicações diretas em prova de teoremas como o Lema de Yoneda e na formalização de transformações naturais.