Strict stability of extension types

Resumo Técnico: Estabilidade Estrita de Tipos de Extensão

Enunciado do Problema
O artigo aborda uma lacuna fundamental no desenvolvimento sintético de $(\infty, 1)$-categorias dentro da Teoria dos Tipos Homotópicos (HoTT), especificamente o sistema introduzido por Riehl e Shulman. Embora a semântica deste sistema tenha sido esboçada utilizando teoria da homotopia simplicial e o modelo de espaço de Segal, a formulação original deixou em aberto a demonstração da estabilidade estrita para tipos de extensão sob substituição. Em modelos de teoria dos tipos, a "estabilidade estrita" exige que a interpretação dos formadores de tipos (como tipos de extensão) comute estritamente com pullbacks (substituição), e não meramente até isomorfismo ou homotopia. Sem essa propriedade, o sistema não pode ser totalmente interpretado na linguagem interna de um $\infty$-topos de uma forma que suporte a igualdade estrita exigida por certas teorias de categorias internas (por exemplo, as de Martini–Wolf).

Metodologia
O autor emprega o método de divisão (splitting method) originalmente descrito por Voevodsky e posteriormente generalizado por Lumsdaine e Warren para universos locais. A abordagem envolve as seguintes etapas técnicas:

1. Categorias de Universo: O trabalho está situado dentro de uma categoria de universo (uma categoria $\mathcal{C}$ equipada com um objeto universo $U$ e uma fibração universal $\pi: \tilde{U} \to U$). O autor assume a existência de uma "divisão" (splitting), que é uma escolha global de quadrados de pullback para a fibração universal. Isso garante que o reindexamento (substituição) seja modelado por igualdade estrita de objetos e morfismos, não apenas por isomorfismo.
2. Contextos Genéricos: Seguindo o estilo do trabalho de Awodey sobre modelos naturais, o artigo define contextos genéricos (objetos classificadores) para a formação e introdução de tipos de extensão.
   • $U_{\text{Ext}@j}$ é definido como o objeto que classifica pares de uma família de tipos $A$ e uma seção parcial $a$ sobre uma inclusão de forma $j: \phi \hookrightarrow \psi$.
   • $U_{\lambda@j}$ é definido como o objeto que classifica trios $\langle A, a, b \rangle$ onde $b$ é uma extensão total de $a$.
3. Construção de Pullback Estrito: O autor constrói o formador de tipo de extensão $\text{Ext}@j$ e o mapa de introdução $\lambda@j$ como morfismos entre esses contextos genéricos e o universo. Ao utilizar a divisão da fibração universal, o artigo demonstra que o quadrado formado por esses mapas é um pullback estrito (não apenas um pullback fraco).
4. Pressupostos de Fibrância: Para simplificar o cenário técnico mantendo a aplicabilidade aos modelos simpliciais padrão, o autor assume que os "formatos" (shapes — os contextos simpliciais) são fibrantes. Isso garante que os cotensores de Leibniz sejam fibrações, permitindo que os tipos de extensão sejam modelados como pullbacks ordinários de 1-categorias.

Principais Contribções e Resultados
A principal contribuição é o Teorema 3.8, que estabelece a estabilidade estrita dos tipos de extensão. O teorema prova que, para um topos de tipo teórico $\mathcal{E}$ e seu associado modelo simplicial $s\mathcal{E}$, uma divisão fixa dos formadores de tipos padrão produz uma interpretação de tipos de extensão que satisfaz as seguintes igualdades estritas para qualquer morfismo de contexto $\sigma: \Delta \to \Gamma$:

1. Estabilidade de Formação: $\sigma^*(\text{Ext}@j(A, a)) = \text{Ext}@j(\sigma^*A, \sigma^*a)$
2. Estabilidade de Introdução: $\sigma^*(\lambda@j_{A,a}(b)) = \lambda@j_{\sigma^*A, \sigma^*a}(\sigma^*b)$
3. Estabilidade de Eliminação: $\sigma^*(\text{app}@j_{A,a}(f, s)) = \text{app}@j_{\sigma^*A, \sigma^*a}(\sigma^*f, \sigma^*s)$

O artigo detalha ainda como as regras de computação $\beta$- e $\eta$- são satisfeitas dentro deste framework de estabilidade estrita, baseando-se na propriedade universal dos quadrados de pullback definidos pela divisão.

Significância e Alegações
O artigo afirma que este resultado resolve o problema em aberto sobre a estabilidade estrita dos tipos de extensão no sistema de Riehl–Shulman. O resultado prático é que o sistema agora possui uma semântica robusta nos objetos simpliciais de um $\infty$-topos. Isso permite o uso do sistema para provar teoremas sobre $\infty$-categorias internas no sentido de Martini–Wolf, pois a estabilidade estrita garante que as operações de teoria dos tipos se alinhem perfeitamente com os pullbacks categóricos exigidos pela teoria de categorias internas.

O autor observa que, embora o trabalho assuma um único universo e formatos fibrantes para simplicidade técnica, acredita-se que o raciocínio se generalize para hierarquias de universos e estruturas fibradas mais complexas sem obstrução essencial. O trabalho serve como uma ponte entre a sintaxe sintética da HoTT simplicial e a semântica rigorosa dos $\infty$-topoi.