The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Sintesi Tecnica: L'Aggiunzione di Leibniz nella Teoria dei Tipi Omotopici

Enunciato del Problema
La teoria dei tipi simpliciali (STT) estende la teoria dei tipi omotopici (HoTT) per fornire un framework sintetico per le categorie superiori, equipaggiando i tipi con morfismi diretti tramite un intervallo. Una sfida centrale in questo campo è definire i "tipi di Segal" (Segal types)—tipi in cui i morfismi diretti possono essere composti. Sebbene la composizione sia immediata, garantire che tale composizione sia associativa e unitaria richiede una gerarchia infinita di coerenze superiori. Nella formulazione standard di STT di Riehl e Shulman, queste coerenze sono spesso gestite tramite costruzioni metateoretiche, rendendo difficile la piena formalizzazione. Nello specifico, dimostrare che un tipo con riempimenti unici per gli $(2,1)$-horn (la condizione base per i tipi di Segal) implica riempimenti unici per tutti gli inner $(n,k)$-horn (generalizzando l'associatività e l'unitarietà della composizione) è non banale. Risultati precedenti, come quelli di Riehl e Shulman, coprivano casi specifici di bassa dimensione ($n=3$), ma una prova generale per tutti gli $n$ e $k$ all'interno di un framework unificato di HoTT rimaneva un ostacolo tecnico aperto.

Metodologia
Gli autori adottano un approccio di teoria dei tipi omotopici "plain", seguendo Gratzer, Weinberger e Buchholtz, piuttosto che l'approccio dell'intervallo meta-teoretico di Riehl e Shulman. Essi postulano un tipo intervallo $I$ che forma un reticolo distributivo limitato, evitando la necessità di ordini totali o modalità specifiche.

L'innovazione tecnica principale è l'internalizzazione dell'aggiunzione di Leibniz all'interno della "categoria selvatgia di tipi" (wild category of types).

1. Categorie Selvagge (Wild Categories): Gli autori lavorano con "categorie selvagge", che sono traduzioni naive della teoria delle categorie in HoTT. Queste mancano di dati di coerenza superiore (le leggi di associatività e identità valgono definizionalmente o non sono tracciate), rendendole distinte dalle $(\infty, 1)$-categorie, ma sufficienti per gli scopi degli autori.
2. L'Aggiunzione: Essi stabiliscono che il prodotto-pushout (indicato con $\hat{\times}$) è aggiunto al pullback-hom (indicato con $\pitchfork$) nella categoria selvatgia delle mappe.
   • Per le mappe $f: A \to B$ e $g: X \to Y$, il prodotto-pushout $f \hat{\times} g$ è la mappa indotta dal pushout di $f \times Y$ e $A \times g$.
   • Il pullback-hom $f \pitchfork g$ è la mappa indotta tra i tipi funzione.
   • L'aggiunzione afferma: $\text{Map}(f \hat{\times} g, h) \simeq \text{Map}(f, g \pitchfork h)$.
3. Mappe vs Famiglie: Una prova diretta di questa aggiunzione nella categoria selvatgia delle mappe è intrattabile a causa della complessità del tracciamento dei dati di coerenza (7-uple di mappe e identificazioni). Per superare ciò, gli autori utilizzano l'assioma di univalenza per stabilire un equivalenza tra la categoria selvatgia delle mappe e la categoria selvatgia delle famiglie (tipi dipendenti). Essi dimostrano che il prodotto-pushout e il pullback-hom corrispondono al join fiberwise e a una specifica costruzione di prodotto dipendente nella categoria delle famiglie, dove l'aggiunzione è più facile da verificare.

Contributi Chiave e Risultati

1. L'Aggiunzione di Leibniz (Teorema 3.16): Il saggio dimostra che il prodotto-pushout e il pullback-hom formano una coppia aggiunta nella categoria selvatgia dei tipi. Questo è un risultato tecnico significativo perché, sebbene ben noto per le 1-categorie, dimostrare ciò per strutture superiori (anche nel contesto "selvaggio") richiede una gestione attenta dell'equivalenza tra mappe e famiglie per evitare un intrattabile bookkeeping della coerenza.
2. Generalizzazione delle Proprietà dei Tipi di Segal (Teorema 4.9): Utilizzando l'aggiunzione di Leibniz, gli autori dimostrano che se un tipo ha riempimenti unici per gli $(2,1)$-horn (ovvero, è un tipo di Segal), esso possiede automaticamente riempimenti unici per tutti gli inner $(n,k)$-horn ($0 < k < n$).
   • Questo generalizza il risultato di Riehl e Shulman (che copriva $n=3$) e fornisce una versione del risultato di Lurie per la teoria dei tipi simpliciali.
   • La prova si basa sul dimostrare che le inclusioni degli inner horn $\lambda^n_k$ sono "inner anodyne" (sinistra-ortogonali a tutti i tipi di Segal). Ciò è ottenuto dimostrando che $\lambda^n_k$ è un ritratto del prodotto-pushout $\lambda^n_k \hat{\times} \lambda^2_1$, e applicando le proprietà di chiusura dell'ortogonalità derivate dall'aggiunzione di Leibniz.
3. Formalizzazione: Tutti i risultati sono formalizzati in Cubical Agda. Il codice è disponibile e serve come verifica degli complessi argomenti combinatori riguardanti indici e pushout.

Significatività e Rivendicazioni
Il saggio sostiene che il suo contributo primario è la riuscita internalizzazione dell'aggiunzione di Leibniz all'interno di HoTT, che funge da potente strumento per derivare coerenze superiori nella teoria dei tipi simpliciali.

• Framework Sintetico: Lavorando con un tipo intervallo interno, gli autori dimostrano che tutte le coerenze superiori per i tipi di Segal possono essere enunciate e derivate sinteticamente all'interno di HoT, senza ricorrere alla quantificazione meta-teoretica.
• Fattibilità della Formalizzazione: Gli autori evidenziano come il loro approccio permetta una completa formalizzazione in Agda. Essi notano che, mentre l'approccio meta-teoretico di Riehl–Shulman potrebbe rendere più facile l'enunciazione del teorema (grazie al ragionamento basato su insiemi a livello meta), la dimostrazione del caso generale nel loro framework interno è non banale e ha richiesto lo sviluppo dell'aggiunzione di Leibniz per gestire la "maggior parte della sfida" riguardante il tracciamento della coerenza.
• Utilità Tecnica: L'equivalenza tra la categoria selvatgia delle mappe e quella delle famiglie è presentata come uno strumento metodologico cruciale che semplifica le prove che coinvolgono il prodotto-pushout e il pullback-hom, rendendo la derivazione delle proprietà di ortogonalità fattibile.

In sintesi, il saggio fornisce una fondazione rigorosa e formalizzata per la teoria dei tipi simpliciali, dimostrando che la condizione base di Segal implica la piena coerenza categorica superiore attraverso l'applicazione dell'aggiunzione di Leibniz in un contesto categorico selvaggio.