The $\infty$-category of $\infty$-categories in simplicial type theory

Resumo Técnico: A $\infty$-categoria de $\infty$-categorias em Teoria de Tipos Simpliciais

Enunciado do Problema
A Teoria de Tipos Simpliciais (STT), introduzida por Riecle e Shulman, fornece um arcabouço sintético para a teoria de $(\infty, 1)$-categorias ao estender a Teoria de Tipos Homotópicos (Hoott) com um intervalo dirigido $I$. Embora a STT defina com sucesso $\infty$-categorias como tipos que satisfazem propriedades específicas (condições de Segal e Rezk) e suporte construções como limites, colimites e categorias fibradas, uma lacuna fundamental permanecia: o universo de tipos $U$ em si não é uma $\infty$-categoria dentro da STT. Especificamente, o subtipo de tipos que satisfazem o predicado $\text{isCat}$ falha em formar uma categoria porque os morfismos sintéticos (funções $I \to \sum_{A:U} \text{isCat}(A)$) não compõem ou representam fielmente funtores. Consequentemente, conjecturou-se que a "categoria de categorias" ($\text{Cat}$) existia como um construto do subtipo do universo, mas ela não havia sido realizada. Essa ausência impedia a internalização de resultados fundamentais como o teorema de endireitamento–desendireitamento (straightening–unstraightening) e dificultava a aplicação da teoria de tipos dirigida a estruturas algébricas superiores.

Metodologia
Os autores constroem $\text{Cat}$ adaptando técnicas da teoria de tipos cubica e da teoria de tipos dependentes modais (MTT) ao contexto da Teoria de Tipos Simpliciais. A metodologia procede através de várias etapas principais:

1. Teoria de Tipos Triangulada ($TT^\triangle$): Os autores trabalham dentro de $TT^\triangle$, uma relaxação da STT onde o intervalo dirigido $I$ é um reticulado distributivo limitado em vez de um conjunto totalmente ordenado. Este modelo (espaços cubicos de Dedekind) admite um "adjunto direito incrível" para o funtor exponencial $I \to (-)$, uma característica ausente em espaços simpliciais padrão, mas crucial para definir fibrações universais.
2. Modalidades: A teoria é estendida com modalidades, especificamente a modalidade $\flat$ (functor discreto) e a modalidade $\sharp$ (functor cocordiscreto). Estas permitem a internalização de elementos globais e a distinção entre grupoides discretos e categorias gerais.
3. Família Cocartesiana Universal: Seguindo Licata et al. e Weaver e Licata, os autores definem $\text{Cat}$ não por um predicado direto sobre tipos, mas como a base de uma família cocartesiana universal. Eles utilizam o Lema 2.9 para transpor predicados definidos sobre $I^n$ (como ser uma fibração interna ou possuir levantamentos localmente cocartesianos) para predicados sobre o universo $U$.
4. Definição de $\text{Cat}$: $\text{Cat}$ é definido como o subtipo de $U$ consistindo de tipos que são Rezk, internos (satisfazendo a condição de Segal relativa) e que possuem levantamentos localmente cocartesianos que compõem.
5. Univalência Dirigida: Os autores provam que $\text{Cat}$ satisfaz um princípio de "univalência dirigida", estabelecendo uma equivalência entre morfismos sintéticos em $\text{Cat}$ e funções entre os tipos subjacentes, mediada pela modalidade $\flat$.

Principais Contribuições e Resultados

• Construção de $\text{Cat}$: A principal contribuição é a primeira construção da $\infty$-categoria de $\infty$-categorias dentro da STT. Os autores definem $\text{Cat}$ como um subtipo do universo e provam que ele é, em si, uma categoria (ou seja, é simplicial, de Segal e Rezk).
• Propriedade Universal (Teorema 4.2): O artigo estabelece que $\text{Cat}$ é a base da família cocartesiana universal. Para qualquer categoria $C$ (especificamente $\flat$-anotada), há uma equivalência:
  $$\langle \flat \mid C \to \text{Cat} \rangle \simeq \langle \flat \mid \sum_{E: C \to U} \text{isCocart}(E) \rangle$$
  Isso caracteriza $\text{Cat}$ via a correspondência de Grothendieck (endireitamento–desendireitamento) puramente através da teoria de tipos.
• Univalência Dirigida (Corolário 5.5): Os autores provam que, para elementos $\flat$ de $A, B$ em $\text{Cat}$, o tipo de morfismos sintéticos é equivalente ao tipo de funções entre eles:
  $$\text{hom}_{\text{Cat}}(A, B) \simeq \langle \flat \mid A \to B \rangle$$
  Este resultado distingue $\text{Cat}$ da categoria de espaços (categorias discretas), onde a equivalência ocorre sem a modalidade $\flat$.
• Endireitamento–Desendireitamento Sintético: Ao analisar as fibras do mapa de desendireitamento $U: (C \to \text{Cat}) \to \text{Cat}/C$, os autores fornecem uma prova totalmente sintética do teorema de endireitamento–desendireamento de Lurie. Eles mostram que a imagem deste mapa consiste precisamente em famílias cocartesianas e funtores cocartesianos.
• Princípio do Homomorfismo de Estrutura (SHP): A construção permite novos exemplos do princípio dirigido da identidade de estrutura. Os autores demonstram como construir categorias complexas, como a categoria de categorias monoidais e a categoria de categorias marcadas, combinando $\text{Cat}$ com conectivos e modalidades de teoria de tipos.

Significância e Alegações
O artigo afirma fechar uma grande lacuna nos fundamentos da Teoria de Tipos Simpliciais. Ao construir $\text{Cat}$, os autores permitem:

1. Internalização da Teoria de Categorias Superiores: Resultados fundamentais, anteriormente exigindo argumentos externos de categoria-modelo, agora podem ser provados sinteticamente dentro da teoria de tipos.
2. Semântica para Teoria de Tipos Dirigida: A existência de $\text{Cat}$ permite uma tradução sintática de teorias de tipos "totalmente dirigidas" para STT, fornecendo um modelo para estas teorias que captura adequadamente as $\infty$-categorias.
3. Novas Construções: O arcabouço facilita a definição de estruturas algébricas complexas (ex: categorias monoidais, $E_1$-monoides) e a aplicação de conceitos de K-teoria algébrica (via definição de grupos K de Quillen) dentro de um ambiente sintético.

Os autores enfatizam que sua abordagem é independente de modelo em sua derivação (recorrendo aos axiomas de $TT^\triangle$), embora seja validada por um modelo em espaços cúbicos. Eles veem este trabalho como um passo para realizar a álgebra superior e a teoria de operads sinteticamente, observando que, embora a construção de $\text{Cat}$ esteja completa, mais trabalho é necessário para explorar plenamente suas aplicações em K-teoria algébrica e para desenvolver uma conta computacional da teoria.