Extension Types for Free

Sintesi Tecnica: Tipi di Estensione "Gratuiti": Cofibrations, Gluing e Univalenza nella Teoria dei Tipi a Due Livelli

Problematica
I tipi di estensione sono un concetto fondamentale nella teoria dei tipi dipendenti, apparendo in vari contesti come le teorie dei tipi cubici (percorsi con endpoint fissi), la teoria dei tipi simpliciali di Riehl e Shulman (termini fissi su sottoshape) o i meccanismi di unfolding controllato. Nei framework esistenti, questi tipi vengono tipicamente postulati come nuovi primitivi, governati da un "calcolo delle facce" meta-teorico o da uno strato di forma che ne determina la formazione e le regole. Questo approccio richiede spesso costruzioni modellistiche specifiche o aggiunte assiomatiche per validare le regole (quali condizioni di confine strette, estensionalità funzionale relativa e la proprietà di estensione dell'omotopia). Un problema centrale nella teoria dei tipi omotopici (HoTT) è determinare la precisa relazione tra la "book HoTT" (la formulazione assiomatica del libro di HoTT) e le teorie dei tipi cubici, in particolare se siano estensioni conservative l'una dell'altra.

Metodologia
Il lavoro utilizza la Teoria dei Tipi a Due Livelli (2LTT) come framework unificante. La 2LTT arricchisce la HoTT con un livello di uguaglianza "stretto" (esterno) che soddisfa l'Unicità delle Prove di Identità (UIP) e l'estensionalità funzionale, mentre il livello "interno" (fibrante) mantiene la struttura omotopica standard.

• Semantica: Il framework è semanticamente "libero"; i modelli standard della HoTT (ad esempio, insiemi simpliciali, insiemi cubici) generano automaticamente modelli di 2LTT tramite costruzioni di presheaf. La teoria è conservativa rispetto al suo livello interno, il che significa che non si possono derivare nel linguaggio interno nuovi teoremi che non fossero già derivabili nella HoTT.
• Definizione di Tipi di Estensione: Invece di postulare i tipi di estensione, il lavoro li definisce internamente alla 2LTT. Data una cofibrazione $i: \Phi \hookrightarrow \Psi$ (una mappa nel livello esterno), una famiglia fibrante $A$ su $\Psi$ e una sezione parziale $a$, il tipo di estensione è definito come la fibra stretta della mappa di restrizione su $a$:
  $$\Pi_\Psi A \mid_i^a \coloneqq \Sigma_{f : \Pi_\Psi A} (f \circ i =_s a)$$
  Qui, $=_s$ denota l'uguaglianza stretta del livello esterno.
• Cofibrations: Il "calcolo delle facce" viene sostituito dalla classe di cofibrations nel livello esterno. Il lavoro tratta la scelta specifica di quali mappe siano cofibrations come un parametro, permettendo al framework di adattarsi a diversi setting (simpliciali, cubici, ecc.) senza cambiare la definizione centrale.

Contributi Chiave e Risultati

1. Tipi di Estensione "Gratuiti":
   Il lavoro dimostra che, nella 2LTT, l'intero calcolo dei tipi di estensione proposto da Riehl e Shulman è definibile piuttosto che assiomatico.

   • Regole Strette: L'introduzione, l'eliminazione, le regole $\beta$, $\eta$ e le regole di confine valgono strettamente per costruzione.
   • Assiomi Dimostrabili: Assiomi che sono postulati in altri contesti, come l'estensionalità funzionale relativa e la proprietà di estensione dell'omotopia (realignment), diventano teoremi derivati dalle proprietà di cofibrations e fibrations nella 2LTT.
   • Unificazione: Questa singola definizione assorbe varie istanze esistenti, inclusi i percorsi cubici, i tipi di estensione di Riehl-Shulman e i tipi indicizzati da proposizioni (unfolding controllato).

2. Equivalenza tra Gluing e Univalenza:
   Il lavoro stabilisce un preciso ciclo di implicazioni che collega il gluing cubico e l'assioma di univalenza all'interno del framework 2LTT:

   • Univalenza $\implies$ Gluing: Se l'universo interno è univalente, allora per ogni cofibrazione, il tipo di "dati di Glue" (strutture richieste per formare un tipo Glue) è contrattile. Ciò implica l'esistenza di una struttura di Glue che soddisfi le regole in forma omotopica.
   • Gluing $\implies$ Univalenza: Viceversa, l'esistenza di una "struttura di Glue debole" (che richiede solo uguaglianze interne per l'accordo dei confini e una struttura di intervallo di percorsi) implica che l'universo sia univalente.
   • Risultato: In presenza di un intervallo di percorsi, l'univalenza e l'esistenza di dati di Glue contrattili sono equivalenti. Questo inverte la direzione standard di implicazione (che vede i tipi Glue implicare la Univalenza) ed estone una doppia equivalenza.

3. Formalizzazione:
   Tutti i risultati dalla Sezione 2 alla Sezione 5 sono auto-formalizzati in Agda utilizzando il flag --two-level. La formalizzazione combina argomenti interni di HoTT con ragionamenti esterni sul livello stretto, verificando la coerenza e la correttezza delle affermazioni teoriche.

4. Approccio alla Conservatività:
   Il lavoro propone una strategia per affrontare il problema aperto se le teorie dei tipi cubici siano conservative rispetto alla book HoTT. Rappresentando entrambi i sistemi all'interno della 2LTT:

   • La Book HoTT è rappresentata come MLTT + Univalenza (livello interno).
   • La Teoria dei Tipi Cubici è rappresentata come MLTT + Glue + Intervallo di Percorsi (assunzioni strutturali/esterne).
   • Il lavoro dimostra che, su una teoria di base con un intervallo di percorsi, l'assioma di Univalenza e l'assioma di Glue sono inter-derivabili. Ciò suggerisce che la differenza fondamentale tra le due teorie possa essere strutturale piuttosto che logica, offrendo una via per dimostrare la conservatività.

Significato e Rivendicazioni
Il lavoro sostiene che il framework dei tipi di estensione fornisce una base uniforme e "gratuita" per i tipi di estensione, eliminando la necessità di assiomi ad hoc o specifiche costruzioni modellistiche per validare le loro regole. Interiorizzando il calcolo delle facce come cofibrations, la teoria unifica diverse occorrenze di tipi di estensione presenti in letteratura.

Riguardo alla connessione tra le teorie dei tipi cubici e la book HoTT, il lavoro è modesto. Non pretende di aver risolto la congettura sulla conservatività. Al contrario, offre una prova di concetto: dimostra che il meccanismo centrale della teoria dei tipi cubici (gluing) è logicamente equivalente all'assioma centrale della HoTT (univalenza) se visto attraverso la lente della 2LTT. Questa equivalenza permette ai ricercatori di tradurre estensioni strutturali (come i tipi Glue) in estensioni assiomatiche all'interno di un unico framework, facilitando il confronto e potenzialmente aprendo la strada a future prove di conservatività. Il lavoro nota esplicitamente che l'assunzione di un "intervallo di percorsi" sul lato HoTT rimane una sfida aperta per ottenere una piena equivalenza.