Directed type theory, with a twist

1. Il Problema

La Teoria dei Tipi Omotopica (HoTT) ha avuto un successo significativo come fondamento della matematica e come linguaggio sintetico per ragionare sugli $\infty$-grupoidi (spazi). Tuttavia, in molte aree della matematica e dell'informatica, le strutture fondamentali non sono i gruppi (o $\infty$-grupoidi), ma le categorie. Le categorie possiedono una direzione intrinseca (morfismi non invertibili), che la HoTT standard non cattura naturalmente.

Sono state proposte diverse "Teorie dei Tipi Dirette" per colmare questa lacuna, ma le soluzioni esistenti presentano compromessi significativi:

1. Mancanza di semplicità semantica: Alcuni approcci (come la Simplicial Type Theory) estendono l'universo dei tipi includendo strutture che non sono categorie, rendendo necessario dimostrare che un tipo costruito è effettivamente una categoria.
2. Assenza di strutture omogenee: Altri approcci non introducono tipi "Hom" (morfismi diretti) come costrutti primitivi, rendendo difficile l'encoding delle $n$-celle e delle coerenze necessarie per la teoria delle categorie superiori.
3. Difficoltà nel ragionamento sui funtori: È stato storicamente difficile generalizzare il concetto di omotopia (tra funzioni) al caso diretto (trasformazioni naturali) mantenendo una sintassi simile a quella della HoTT.

L'obiettivo del lavoro è definire una nuova teoria dei tipi diretti che soddisfi tre requisiti fondamentali (desiderata):

1. I tipi chiusi devono essere semanticamente categorie.
2. Deve esistere un tipo di "uguaglianze dirette" (Hom-type) con regole di formazione, introduzione, eliminazione e computazione.
3. Le uguaglianze dirette devono essere introdotte tramite "oggetti di percorso diretti" che permettano di ragionare sulle trasformazioni naturali.

2. Metodologia

Gli autori adottano un approccio semantico basato su modelli categoriali, estendendo il modello di North (che generalizza il modello di gruppoide di Hofmann-Streicher). La metodologia si articola in tre fasi principali:

• Modelli di Categoria e Categorie Esibite (Displayed Categories):
  Utilizzano un modello di comprensione (Comprehension Category) dove i contesti sono categorie e i tipi sono categorie indicizzate. Introducono un secondo livello di sintassi per le "tipi esibiti" (displayed types), che corrispondono a funtori arbitrari su una categoria base, permettendo di modellare proiezioni che non sono necessariamente op-fibrations (come la proiezione dalla categoria delle frecce).

• L'Operazione di "Twist" (Torcimento):
  Il contributo centrale è l'introduzione di un'operazione sintattica chiamata "twist". Data una tipologia che dipende sia covariantemente che controvariantemente da alcune variabili, l'operazione di twist produce un nuovo tipo che dipende solo covariantemente dalle stesse variabili.

  • Ispirazione: Questa operazione è ispirata alla costruzione di Grothendieck per i profunctori di Street.
  • Meccanismo: Trasforma un tipo del tipo $\Gamma, b: B^{op}, a: A \vdash C$ in un tipo esibito $\Gamma, b: B, a: A \vdash C[\bar{b}/b]^{d}$.

• Fibrati 2-laterali Dipendenti (D2SFibs):
  Per dare semantica all'operazione di twist, gli autori generalizzano il concetto di 2-sided fibration di Street. Introducono i Dependent 2-sided Fibrations (D2SFibs), che sono strutture che combinano proprietà di fibrato e op-fibrato in modo dipendente. Dimostrano un teorema di "straightening-unstraightening" che stabilisce un'equivalenza tra profunctori dipendenti e D2SFibs.

3. Contributi Chiave

1. Twisted Type Theory (TTT):
   Viene presentata una nuova teoria dei tipi che estende la MLTT (Martin-Löf Type Theory) con:

   • Tipi omogenei (Hom-types) con regole di introduzione ed eliminazione modificate.
   • L'operazione di "Twist" sui tipi.
   • Tipi esibiti, contesti opposti e universi di tipi discreti.

2. Regola di Introduzione per Hom-types:
   Grazie al twist, gli autori possono formulare una regola di introduzione per i tipi Hom ($\text{refl}_d$) che è sintatticamente analoga alla regola di introduzione dell'identità in HoTT, ma la cui interpretazione semantica corrisponde alla fattorizzazione della mappa diagonale attraverso la categoria delle frecce ($A^\to$). Questo soddisfa il terzo desiderato, permettendo di ragionare sulle trasformazioni naturali.

3. Regola di Eliminazione per Hom-types:
   Viene proposta una regola di eliminazione che generalizza l'eliminazione di J di HoTT. Questa regola specifica che il "motive" (la proprietà da dimostrare) può dipendere da una variabile aggiuntiva di forma appropriata, permettendo di gestire la mancanza di tutti i tipi $\Pi$ (prodotti dipendenti) nel modello di categoria.

4. Caratterizzazione delle Strutture Categoricali:

   • I tipi twistati permettono di caratterizzare sintatticamente le trasformazioni naturali.
   • Viene dimostrata una versione della "univalence diretta" per insiemi (Set), dove il tipo di funzioni $A \to B$ è isomorfo al tipo Hom tra insiemi.
   • Viene mostrato come i tipi twistati si relazionino ai tipi $\Sigma$ e $\Pi$ e agli endi lassi (lax ends).

4. Risultati Principali

• Validazione Semantica: Il modello di categoria soddisfa tutte le regole di TTT. In particolare, l'interpretazione del twist del tipo Hom di un tipo $A$ restituisce esattamente la categoria delle frecce $A^\to$.
• Dimostrazione Sintetica del Lemma di Yoneda:
  Gli autori utilizzano TTT per fornire una prova sintetica del Lemma di Yoneda. La prova dimostra che i due funtori $Y(F, a) = \text{Nat}(\text{Hom}(a, -), F)$ e $\bar{Y}(F, a) = F(a)$ sono naturalmente isomorfi.
  • La dimostrazione sfrutta la regola di eliminazione Hom per costruire le trasformazioni naturali necessarie, mostrando come la struttura di TTT catturi l'essenza del lemma senza ricorrere a costruzioni semantiche esterne.
• Gestione delle Trasformazioni Naturali:
  Viene dimostrato che i termini del tipo twistato $\text{Hom}(F(a), G(a))$ corrispondono esattamente alle trasformazioni naturali tra i funtori $F$ e $G$, risolvendo un problema aperto in precedenti teorie dirette.

5. Significato e Impatto

Il lavoro di Chu e North rappresenta un passo significativo verso una fondazione unificata per la teoria delle categorie all'interno della teoria dei tipi:

• Sintesi tra Sintassi e Semantica: TTT riesce a mantenere una sintassi vicina alla HoTT (permettendo tecniche di prova familiari) mentre la sua semantica è rigorosamente basata sulle categorie, non sui gruppioidi.
• Semplificazione della Costruzione di Categorie: A differenza di approcci come la Simplicial Type Theory, in TTT ogni tipo chiuso è automaticamente una categoria. Questo elimina la necessità di prove aggiuntive per verificare che una costruzione sia una categoria.
• Fondamento per la Teoria delle Categorie Superiori: Sebbene il lavoro si concentri sul caso 1-dimensionale (categorie), l'introduzione dei tipi Hom e delle regole di eliminazione fornisce la base necessaria per estendere la teoria a dimensioni superiori ($\infty$-categorie), dove le coerenze emergono naturalmente dalle regole di eliminazione.
• Nuovo Strumento per la Matematica Sintetica: La capacità di ragionare su trasformazioni naturali e il Lemma di Yoneda direttamente nel linguaggio dei tipi apre la strada a nuove forme di verifica formale e sviluppo di teoremi nella teoria delle categorie.

In conclusione, la "Twisted Type Theory" offre un compromesso elegante tra la semplicità dei modelli di gruppoide e la ricchezza delle strutture categoriali, introducendo l'operazione di "twist" come meccanismo chiave per colmare il divario tra la dipendenza covariante e controvariante.