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

Sintesi Tecnica: La $\infty$-categoria delle $\infty$-categorie nella Teoria dei Tipi Simpliciali

Enunciato del Problema
La Teoria dei Tipi Simpliciali (STT), introdotta da Riehl e Shulman, fornisce un quadro sintetico per la teoria delle $(\infty, 1)$-categorie estendendo la Teoria dei Tipi Omotopici (HoTT) con un intervallo diretto $I$. Sebbene la STT definisca con successo le $\infty$-categorie come tipi che soddisfano specifiche proprietà (condizioni di Segal e Rezk) e supporti costruzioni come limiti, colimiti e categorie fibrate, rimaneva una lacuna fondazionale: l'universo dei tipi $U$ stesso non è una $\infty$-categoria all'interno della STT. Nello specifico, il sottotipo di tipi che soddisfano il predicato di $\infty$-categoria ($\text{isCat}$) non forma una categoria perché i morfismi sintetici (funzioni $I \to \sum_{A:U} \text{isCat}(A)$) non compongono o non rappresentano fedelmente i funtori. Di conseguenza, si era ipotizzato che la "categoria delle categorie" ($\text{Cat}$) fosse un costrutto sottotipo dell'universo, ma non era stata ancora realizzata. Questa assenza impediva l'internalizzazione di risultati fondamentali come il teorema di raddrizzamento–diradamento (straightening–unstraightening) e ostacolava l'applicazione della teoria dei tipi diretti alle strutture algebriche superiori.

Metodologia
Gli autori costruiscono $\text{Cat}$ adattando le tecniche della teoria dei tipi cubici e della teoria dei tipi modali dipendenti (MTT) al contesto della Teoria dei Tipi Simpliciali. La metodologia procede attraverso diverse fasi chiave:

1. Teoria dei Tipi Triangolata ($TT^\triangle$): Gli autori lavorano all'interno di $TT^\triangle$, un rilassamento della STT in cui l'intervallo diretto $I$ è un reticolo distributivo limitato piuttosto che un insieme totalmente ordinato. Questo modello (spazi cubici di Dedekind) ammette un "straordinario amato destroro" (amazing right adjoint) rispetto al funtore esponenziale $I \to (-)$, una caratteristica assente negli spazi simpliciali standard ma cruciale per definire fibrati universali.
2. Modalità: La teoria è estesa con modalità, specificamente la modalità $\flat$ (funzione discreta) e la modalità $\sharp$ (funzione codiscreta). Queste permettono l'internalizzazione degli elementi globali e la distinzione tra groupoid discreti e categorie generali.
3. Famiglia Cocartesiana Universale: Seguendo Licata et al. e Weaver e Licica, gli autori definiscono $\text{Cat}$ non tramite un diretto predicato sui tipi, ma come la base di una famiglia cocartesiana universale. Utilizzano il Lemma 2.9 per trasporre i predicati definiti su $I^n$ (come essere una fibrazione interna o avere sollevamenti localmente cocartesiani) in predicati sul universo $U$.
4. Definizione di $\text{Cat}$: $\text{Cat}$ è definito come il sottotipo di $U$ costituito dai tipi che sono Rezk, interni (che soddisfano la condizione di Segal relativa) e che possiedono sollevamenti localmente cocartesiani che compongono.
5. Univalenza Diretta: Gli autori dimostrano che $\text{Cat}$ soddisfa un principio di "univalenza diretta", stabilendo un'equivalenza tra i morfismi sintetici in $\text{Cat}$ e le funzioni tra i tipi sottostanti, mediata dalla modalità $\flat$.

Contributi Chiave e Risultati

• Costruzione di $\text{Cat}$: Il contributo primario è la prima costruzione della $\infty$-categoria delle $\infty$-categorie all'interno della STT. Gli autori definiscono $\text{Cat}$ come un sottotipo dell'universo e dimostrano che esso è esso stesso una categoria (ovvero è simpliciale, di Segal e Rezk).
• Proprietà Universale (Teorema 4.2): L'articolo stabilisce che $\text{Cat}$ è la base della famiglia cocartesiana universale. Per ogni categoria $C$ (specificamente $\flat$-annotata), esiste un'equivalenza:
  $$\langle \flat \mid C \to \text{Cat} \rangle \simeq \langle \flat \mid \sum_{E: C \to U} \text{isCocart}(E) \rangle$$
  Questo caratterizza $\text{Cat}$ tramite la corrispondenza di Grothendieck (straightening–unstraightening) puramente tipologica.
• Univalenza Diretta (Corollario 5.5): Gli autori dimostrano che per gli elementi $\flat$ di $A, B$ in $\text{Cat}$, il tipo dei morfismi sintetici è equivalente al tipo delle funzioni tra di essi:
  $$\text{hom}_{\text{Cat}}(A, B) \simeq \langle \flat \mid A \to B \rangle$$
  Questo risultato distingue $\text{Cat}$ dalla categoria degli spazi (categorie discrete), dove l'equivalenza si tiene senza la modalità $\flat$.
• Raddrizzamento–Diradamento Sintetico: Analizzando le fibre della mappa di diradamento $U: (C \to \text{Cat}) \to \text{Cat}/C$, gli autori forniscono una prova interamente sintetica del teorema di raddrizzamento–diradamento di Lurie. Dimostrano che l'immagine di questa mappa consiste precisamente di famiglie cocartesiane e funtori cocartesiani.
• Principio di Omomorfismo di Struttura (SHP): La costruzione permette nuovi esempi della versione diretta del principio di identità della struttura. Gli autori dimostrano come costruire categorie complesse, come la categoria delle categorie monoidali e la categoria delle categorie marcate, combinando $\text{Cat}$ con connettivi e modalità tipologiche.

Significato e Rivendicazioni
L'articolo sostiene di colmare una lacuna fondamentale nella Teoria dei Tipi Simpliciali. Costruendo $\text{Cat}$, gli autori permettono di:

1. Internalizzare la Teoria delle Categorie Superiori: Grandi risultati fondazionali, precedentemente richiedenti argomenti esterni di categoria-modello, possono ora essere provati sinteticamente all'interno della teoria dei tipi.
2. Semantica per la Teoria dei Tipi Diretta: L'esistenza di $\text{Cat}$ permette una traduzione sintattica di teorie dei tipi "completamente dirette" in STT, fornendo un modello per queste teorie che cattura adeguatamente le $\infty$-categorie.
3. Nuove Costruzioni: Il framework facilita la definizione di strutture algebriche complesse (ad esempio, categorie monoidali, $E_1$-monoidi) e l'applicazione di concetti di K-teoria algebrica (tramite la definizione di gruppi K di Quillen) in un contesto sintetico.

Gli autori sottolineano che il loro approccio è indipendente dal modello nella sua derivazione (facendo affidamento sugli assiomi di $TT^\triangle$) pur essendo validato da un modello in spazi cubici. Essi vedono questo lavoro come un passo verso la realizzazione della algebra superiore e della teoria degli operadi in modo sintetico, notando che, sebbene la costruzione di $\text{Cat}$ sia completa, è necessario ulteriore lavoro per esplorare pienamente le sue applicazioni nella K-teoria algebrica e per sviluppare un account computazionale della teoria.