Univalent Enriched Categories and the Enriched Rezk Completion

Sintesi Tecnica: Categorie Arricchite Univalenti e il Completamento di Rezk Arricchito

Problematica
La teoria delle categorie è un quadro fondamentale per la matematica e l'informatica, con le categorie arricchite che svolgono un ruolo critico nella teoria delle categorie superiori, nella teoria dell'omotopia e nella semantica dei linguaggi di programmazione (ad esempio, utilizzando i DCPO per i linguaggi con effetti). Tuttavia, nel contesto delle Fondazioni Univalenti (Homotopy Type Theory), la definizione standard di categorie spesso non soddisfa il principio di equivalenza, il quale afferma che gli oggetti isomorfi dovrebbero essere indistinguibili. Sebbene le "categorie univalenti" (dove l'identità degli oggetti è equivalente all'isomorfismo) siano state stabilite per le categorie ordinarie, la teoria delle categorie arricchite univalenti rimane sottosviluppata. Nello specifico, vi è una mancanza di risultati formalizzati riguardanti il principio di identità della struttura, la caratterizzazione delle equivalenze e l'esistenza di un completamento di Rezk (una riflessione univalente) per le categorie arricchite. Inoltre, costruzioni standard come le categorie di Kleisli spesso non sono univalenti, rendendo necessaria una metodologia per costruire analoghi univalenti nell'ambito arricchito.

Metodologia
Il saggio sviluppa la teoria delle categorie arricchite all'interno dell'assistente di prova Rocq utilizzando la libreria UniMath, aderendo alle Fondazioni Univalenti. L'approccio metodologico centrale prevede:

1. L'Arricchimento come Struttura: Invece di definire le categorie arricchite come una collezione di oggetti e oggetti-om (la definizione di Kelly), gli autori definiscono esse come una categoria insieme a un arricchimento. Un arricchimento consiste di oggetti-om in una categoria monoidale $\mathcal{V}$, morfismi di identità e composizione, e una corrispondenza tra i morfismi nella categoria sottostante e gli elementi degli oggetti-om. Questa prospettiva tratta una categoria arricchita come una categoria univalente dotata di struttura extra.
2. Bicategorie Visualizzate (Displayed Bicategories): Per dimostrare il principio di identità della struttura, gli autori utilizzano la strumentazione delle bicatregorie visualizzate. Definiscono una bicategoria visualizzata $dEnrichCat_{\mathcal{V}}$ sopra la bicategoria delle categorie univalenti ($UnivCat$). La bicategoria totale del loro display è $EnrichCat_{\mathcal{V}}$. Ciò consente di riutilizzare i risultati di univalenza esistenti per $UnivCat$ per dimostrare l'univalenza per l'ambito arricchito.
3. Sistemi di Fattorizzazione Ortogonale: Per caratterizzare le equivalenze, il saggio impiega sistemi di fattorizzazione ortogonale nelle bicatregorie. Definisce i funtori arricchiti pienamente immersi ed essenzialmente suriettivi e dimostra che essi formano un sistema di fattorizzazione ortogonale.
4. Due Costruzioni del Completamento di Rezk: Il saggio fornisce due diverse costruzioni per il completamento di Rezk di una categoria arricchita:
   • Imbologamento di Yoneda: Costruire il completamento come l'immagine dell'imbologamento di Yoneda arricchito. Ciò richiede che $\mathcal{V}$ sia completa e simmetrica monoidale chiusa, ma si basa sulla teoria delle categorie standard.
   • Tipi Induttivi Superiori (HITs): Costruire il completamento dotando il completamento di Rezk della categoria sottostante di un arricchimento utilizzando le regole di eliminazione dei HIT. Questo approccio evita assunzioni di completezza o chiusura in $\mathcal{V}$ e preserva i livelli di universo se l'universo è chiuso rispetto ai HIT.
5. Proprietà Universali: Il saggio stabilisce la proprietà universale del completamento di Rezk, dimostrando che la precomposizione con una equivalenza debole (un funtore pienamente immerso ed essenzialmente suriettivo) induce un'equivalenza avversaria tra le categorie di funtori.

Contributi Chiave e Risultati

• Principio di Identità della Struttura: Il saggio dimostra che la bicategoria delle categorie arricchite univalenti ($EnrichCat_{\mathcal{V}}$) è univalente (Teorema 2.8). Ciò implica che il tipo di identità tra due categorie arricchite univalenti è equivalente al tipo delle equivalenze avversarie tra di esse.
• Caratterizzazione delle Equivalenze: Si dimostra che ogni funtore arricchito che è sia pienamente immerso che essenzialmente suriettivo è un'equivalenza avversaria (Teorema 4.8). Questo risultato è costruttivo e si basa sul fatto che dominio e codominio siano univalenti, evitando l'assioma della scelta.
• Completamento di Rezk: Sono fornite due costruzioni per il completamento di Rezk delle categorie arricchite (Costruzioni 5.5 e 5.7). Il saggio dimostra che ogni categoria arricchita ammette un completamento di Rezk e soddisfa la proprietà universale per cui ogni funtore verso una categoria univalente si estende unicamente lungo le equivalenze deboli (Teorema 5.2).
• Categorie di Kleisli Univalenti: Gli autori costruiscono categorie di Kleisli arricchite univalenti. Definiscono la categoria di Kleisli standard $K(T)$ e il suo analogo univalente $Kleisli(T)$ (come una sottocategoria piena della categoria di Eilenberg-Moore). Utilizzando il completamento di Rezk e la proprietà universale, mostrano che $Kleisli(T)$ soddisfa la proprietà universale degli oggetti di Kleisli nella bicategoria delle categorie arricchite univalenti (Costruzione 6.9).
• Esempi e Caratterizzazioni: Il saggio fornisce numerosi esempi, inclusi l'auto-arricchimento, gli arricchimenti opposti e i cambiamenti di base. Caratterizza gli arricchimenti su strutture cartesiane (come i DCPO) e introduce una nozione di "struttura chiusa che supporta i prodotti smash" per gestire insiemi puntati e l'ordine parziale, pur notando le limitazioni riguardo ai DCPO puntati.

Significato e Rivendicazioni
Il saggio sostiene di aver stabilito una fondazione robusta per la teoria delle categorie arricchite all'interno delle Fondazioni Univalenti. Il suo significato primario risiede in:

1. Formalizzazione: Fornire una libreria formalizzata in Rocq/UniMath per le categorie arricchite, che precedentemente mancava di una formalizzazione estesa rispetto alle categorie ordinarie.
2. Correttezza della Nozione: Dimostrare che vedere le categorie arricchite come categorie univalenti con struttura extra (tramite gli arricchimenti) semplifica le dimostrazioni di proprietà fondamentali come il principio di identità della struttura.
3. Risoluzione della Non-Univalenza: Affrontare il problema per cui le costruzioni comuni (come le categorie di Kleisli) non sono intrinsecamente univalenti, fornendo un metodo sistematico (completamento di Rezk) per ottenere versioni univalenti che preservino le necessarie proprietà universali.
4. Strumenti Fondativi: Stabilire la bicategoria delle categorie arricchite univalenti come una bicategoria univalente, che è un prerequisito per lo sviluppo di ulteriore teoria delle categorie interna (ad esempio, monadi, limiti) in un ambito univalente.

Gli autori osservano che, sebbene il loro approccio copra molti casi standard, presenta delle limitazioni riguardo ai prodotti smash per certe strutture (come i DCPO puntati) dove i quozienti devono essere presi nella categoria appropriata piuttosto che negli insiemi. Suggeriscono che il lavoro futuro potrebbe comportare lo sviluppo dell'equipaggiamento delle categorie arricchite o la generalizzazione della nozione di prodotto smash per gestire questi casi.