The internal languages of univalent categories

Sintesi Tecnica: I Linguaggi Interni delle Categorie Univalenti

Problema
I teoremi sui linguaggi interni nella logica categoriale stabiliscono un'equivalenza tra sintassi (teorie dei tipi) e semantica (modelli categoriali). Un risultato fondamentale di Clairambault e Dybjer [CD14] ha corretto il teorema originale di Seely [See84], stabilendo una biequivalenza tra la bicategoria delle categorie localmente cartesiane chiuse (LCCC) e la bicategoria delle categorie democratiche con famiglie (CwF) che supportano tipi di identità estensionali, tipi $\Sigma$ e tipi $\Pi$.

Tuttavia, questo risultato è stato formulato all'interno di fondazioni teoria degli insiemi. Nelle fondazioni univalenti (Teoria dei Tipi Omotopica), la nozione standard di CwF incontra un ostacolo fondamentale: l'assioma di univalenza implica che il tipo degli insiemi non è esso stesso un insieme (è un 1-tipo). Di conseguenza, il requisito nelle CwF secondo cui la collezione di tipi in un contesto formi un insieme viene violato dalla categoria univalente degli insiemi. Inoltre, la distinzione tra struttura "scelta" (ad esempio, fibrazioni split) e struttura "esistente" (ad esempio, limiti fino all'isomorfismo) crea problemi di coerenza nelle fondazioni della teoria degli insiemi che richiedono l'assioma della scelta o procedure di strictificazione. Nelle fondazioni univalenti, dove l'isomorfismo implica l'identità, queste distinzioni evaporano, ma l'attuale framework delle CwF non è direttamente applicabile.

Metodologia
Il saggio sviluppa un nuovo framework per la semantica categoriale all'interno delle fondazioni univalenti, utilizzando categorie univalenti e categorie di comprensione invece delle CwF.

1. Categorie Univalenti: L'autore lavora con categorie in cui il tipo di identità degli oggetti è equivalente al tipo degli isomorfismi (equivalenze avversarie). Ciò consente di trattare le equivalenze avversarie come identità, semplificando le prove riguardanti la preservazione della struttura (ad esempio, gli esponenziali) ed eliminando la necessità dell'assioma della scelta per selezionare i limiti.
2. Categorie di Comprensione: Per modellare i tipi dipendenti senza richiedere che i tipi formino un insieme, il saggio adotta le categorie di comprensione (basate su fibrati e categorie visualizzate). Una categoria di comprensione consiste in una categoria di base dei contesti, una categoria visualizzata dei tipi, un cleaving (che fornisce la sostituzione) e un funtore di comprensione. L'autore restringe l'attenzione alle categorie di comprensione complete univalenti, dove sia la categoria di base che la categoria visualizzata sono univalenti.
3. Bicategorie Visualizzate: La costruzione delle bicategorie di modelli si basa pesantemente sulle bicategorie visualizzate [AFM+21]. Questo approccio modulare permette all'autore di costruire bicategorie complesse (come quelle di LCCC o topos con universi) stratificando le proprietà (ad esempio, limiti finiti, tipi $\Pi$, universi) sopra più semplici categorie di base. Questa modularità facilita la prova che le bicategorie risultanti siano esse stesse univalenti.
4. Proprietà Locali: Per estendere i risultati dalle categorie con limiti finiti a strutture più complesse come i topos, il saggio adatta la nozione di proprietà locali di Maietti [Mai05]. Una proprietà locale è una condizione sulle categorie chiusa rispetto al slicing. L'autore formalizza questo concetto all'interno del framework delle bicategorie visualizzate per estendere le biequivalenze dal caso base (limiti finiti) a varie classi di topos.
5. Rindessizzazione e Universi: Per il trattamento degli universi, il saggio impiega la rindessizzazione di bicategorie visualizzate. Questa tecnica permette di trasferire una biequivalenza da una categoria di base a una categoria visualizzata su di essa, consentendo la definizione di universi chiusi sotto specifici costruttori di tipi (ad esempio, $\Sigma$, $\Pi$, numeri naturali), senza richiedere leggi di stabilità strette, bensì stabilità fino all'isomorfismo (che diventa identità nelle categorie univalenti).

Contributi Chiave
Il saggio apporta quattro contributi primari:

1. Analogo Univalente di Clairambault-Dybjer: L'autore costruisce una biequivalenza tra la bicategoria delle categorie univalenti con limiti finiti e la bicategoria delle categorie di comprensione democratiche a limiti finiti (DFL) univalenti complete. Ciò stabilisce che il linguaggio interno delle categorie univalenti con limiti finiti è la teoria dei tipi di Martin-Löf estensionale con unità, prodotto binario e tipi $\Sigma$.
2. Estensione alle Categorie Localmente Cartesian Closed: La biequivalenza è estesa alle categorie univalenti localmente cartesiane chiuse e alle categorie di comprensione DFL che supportano tipi $\Pi$. Ciò conferma che il linguaggio interno delle LCCC univalenti è la teoria dei tipi di Martin-Löf estensionale con tipi $\Pi$.
3. Estensione a Topos e Universi: Il metodo è generalizzato a varie classi di topos (pretopos, $\Pi$-pretopos, topos elementari, e topos con un oggetto dei numeri naturali) utilizzando le proprietà locali. Inoltre, l'autore definisce gli universi in queste categorie che sono chiusi sotto i costruttori di tipi (numeri naturali, classificatore di sottogruppi, riduzione dimensionale proposizionale, tipi $\Sigma$ e tipi $\Pi$), stabilendo una biequivalenza per i topos elementari con un universo.
4. Formalizzazione: Tutte le costruzioni e le prove sono formalizzate nel assistente di prova Rocq utilizzando la libreria UniMath, garantendo la correttezza e fornendo un riferimento verificato dalla macchina per la teoria.

Risultati
Il saggio dimostra che per varie classi di categorie univalenti, esiste una biequivalenza con le corrispondenti classi di categorie di comprensione univalenti. Nello specifico:

• Limiti Finiti: Categorie univalenti con limiti finiti $\simeq$ categorie di comprensione DFL (Unità, Prodotto, Equalizzatore, $\Sigma$).
• LCCC: LCCC univalenti $\simeq$ categorie di comprensione DFL con tipi $\Pi$.
• Topos: Topos elementari univalenti (con/senza NNO) $\simeq$ categorie di comprensione DFL con le corrispondenti proprietà locali (ad esempio, classificatori di sottogruppi, somme disgiunte, quozienti).
• Universi: Topos elementari univalenti con un universo chiuso sotto specifici costruttori di tipi $\simeq$ categorie di comprensione DFL con un oggetto universo che soddisfa le corrispondenti condizioni di chiusura.

Il saggio dimostra che, nelle fondazioni univalenti, il linguaggio interno di queste strutture categoriali è la teoria dei tipi di Martin-Löf estensionale. L'uso di categorie univalenti semplifica la teoria eliminando la necessità di fibrati split; i problemi di coerenza che affliggono i modelli della teoria degli insiemi (dove la sostituzione deve essere stretta) sono risolti perché gli isomorfismi sono identità.

Significato e Rivendicazioni
Il saggio sostiene che il suo sviluppo fornisce una nuova prospettiva sulla semantica della teoria dei tipi dipendenti. Utilizzando le categorie univalenti, l'autore evita l'overhead tecnico delle fibrazioni split e dell'assioma della scelta, necessari nelle fondazioni della teoria degli insiemi per garantire la correttezza. I principi di identità della struttura inerenti alle fondazioni univalenti permettono un trattamento più naturale delle strutture categoriali in cui gli oggetti sono identificati fino all'equivalenza piuttosto che tramite uguaglianza stretta.

L'autore afferma esplicitamente di non costruire la sintassi o il modello iniziale in questo lavoro; piuttosto, si concentra sul lato categoriale del teorema del linguaggio interno (l'equivalenza tra i modelli). Nota che, sebbene le categorie di comprensione siano adatte alle fondazioni univalenti, altre strutture come le CwF non lo sono, a causa della restrizione di insieme sui tipi. Il saggio si pone come un passo fondativo, lasciando lo sviluppo di una sintassi adeguata (come la sintassi dei groupoid) e la sua interpretazione come lavoro futuro. Il significato risiede nello stabilire una corrispondenza robusta e verificata dalla macchina tra strutture categoriali univalenti e teorie dei tipi, dimostrando che le fondazioni univalenti supportano naturalmente questi teoremi del linguaggio interno senza i difetti presenti nelle precedenti formulazioni della teoria degli insiemi.