Univalence without function extensionality

1. Enunciato del Problema

Il lavoro affronta una domanda fondamentale nella Teoria dei Tipi di Omotopia (HoTT) riguardante la relazione logica tra Univalenza (UA) ed Estendibilità delle Funzioni (FE).

• Contesto: È un teorema standard (dovuto a Voevodsky) che in qualsiasi universo univalente vale l'estendibilità delle funzioni. Cioè, se due funzioni sono omotope ($f \sim g$), allora sono uguali ($f = g$).
• La Domanda: Vale il viceversa? Nello specifico, una forma più debole di univalenza, che asserisce che l'universo forma una "categoria selvaggia univalente" (dove l'uguaglianza dei tipi corrisponde all'esistenza di inversi stretti, ovvero equivalenze categoriali), implica l'estendibilità delle funzioni?
• Contesto: François G. Dorais ha proposto un indebolimento chiamato Univalenza Categorical (CUA), dove la mappa dall'uguaglianza dei tipi all'equivalenza categoriale (mappe con inversi sinistri e destri stretti) è un'equivalenza. Gli autori investigano se CUA implichi FE.

2. Metodologia

Gli autori impiegano la costruzione del modello polinomiale di Von Glehn ($Poly(\mathcal{C})$) per costruire un controesempio. Questo metodo è una fonte nota di modelli per la Teoria dei Tipi di Martin-Löf (ITT) che confutano l'estendibilità delle funzioni.

• Modello di Base ($\mathcal{C}$): Iniziano con un modello $\mathcal{C}$ di ITT che soddisfa l'Univalenza e l'Estendibilità delle Funzioni (ad esempio, un modello cubico) e possiede coprodotto finiti estensivi che soddisfano regole $\eta$ strette.
• Costruzione del Modello Polinomiale: Costruiscono il modello polinomiale $Poly(\mathcal{C})$. In questo modello:
  • I tipi sono coppie $(S, P)$ che rappresentano "forme" e "posizioni".
  • La costruzione è correlata all'interpretazione Dialectica di Gödel e alla categoria dei contenitori.
  • Crucialmente, è noto che $Poly(\mathcal{C})$ confuta sempre FE.
• Analisi degli Isomorfismi: Il lavoro tecnico centrale consiste nell'analizzare la struttura degli isomorfismi (equivalenze categoriali) all'interno del modello polinomiale. Gli autori decompongono il tipo degli isomorfismi tra due tipi nel modello polinomiale in:
  1. Isomorfismi tra i loro componenti "forma" (nel modello di base $\mathcal{C}$).
  2. Isomorfismi tra i loro componenti "posizione", condizionati all'isomorfismo della forma.

3. Definizioni e Concetti Chiave

• Categoria Selvaggia: Una struttura che cattura la natura $(\infty, 1)$-categorica dei tipi, dove composizione e identità soddisfano leggi di coerenza fino all'uguaglianza (non necessariamente omotopia).
• Equivalenza Categorical ($A \sim= B$): Una mappa $f: A \to B$ dotata di inversi sinistri e destri stretti ($sf = id, fs = id$). Questo differisce da un'equivalenza omotopica ($A \simeq B$), dove gli inversi esistono solo fino all'omotopia.
• Univalenza Categorical (CUA): Il principio secondo cui la mappa $(A = B) \to (A \sim= B)$ è un'equivalenza.
• Univalenza Categorical Familiare (CUA$^\bullet$): Una variante più forte che asserisce che, per qualsiasi tipo indice $I$, la categoria delle famiglie indicizzate da $I$ è univalente nel senso categoriale.
• Decomposizione dell'Univalenza: Il lavoro stabilisce che l'Univalenza standard (UA) è logicamente equivalente alla congiunzione di Univalenza Categorical (CUA) ed Estendibilità delle Funzioni (FE).
  $$UA \iff (CUA \land FE)$$

4. Contributi e Risultati Chiave

A. Indipendenza di CUA e FE

Il risultato primario è la dimostrazione che l'Univalenza Categorical Familiare non implica l'Estendibilità delle Funzioni.

• Teorema: $ITT + CUA^\bullet_U \nvdash FE_U$.
• Strategia di Dimostrazione:
  1. Prendere un modello di base $\mathcal{C}$ che soddisfa $UA + FE$.
  2. Costruire $Poly(\mathcal{C})$.
  3. Preservazione di CUA: Gli autori dimostrano (Teorema 4.17) che se il modello di base $\mathcal{C}$ soddisfa l'Univalenza Categorical Familiare, allora anche il modello polinomiale $Poly(\mathcal{C})$ la soddisfa. Questo si basa sul fatto che gli isomorfismi nel modello polinomiale sono determinati dagli isomorfismi nel modello di base (forme) e da condizioni specifiche sulle posizioni che sono contraibili quando il modello di base è univalente.
  4. Confutazione di FE: È una proprietà nota dei modelli polinomiali (Proposizione 5.3) che essi confutano l'Estendibilità delle Funzioni.
  5. Conclusione: $Poly(\mathcal{C})$ è un modello di $ITT + CUA^\bullet_U + \neg FE_U$.

B. Gerarchia delle Varianti di Univalenza

Il lavoro esplora il panorama degli assiomi di univalenza indeboliti, mostrando che non sono tutti equivalenti:

• CUA vs. CUA$^\bullet$: Gli autori mostrano che CUA (per un singolo universo) non implica l'Univalenza Categorical Familiare (CUA$^\bullet$). Costruiscono un modello a fetta in cui CUA vale ma CUA$^\bullet$ fallisce.
• Univalenza Categorical Categorical (CCUA): Definiscono una variante in cui la mappa $(A=B) \to (A \sim= B)$ è un'equivalenza categoriale piuttosto che un'equivalenza omotopica. Mostrano che questa è strettamente più forte di CUA ma comunque non implica FE.
• Univalenza Approssimata: Discutono la "univalenza approssimata" di Van den Berg (esistenza di un percorso per ogni equivalenza) e notano che la sua relazione con FE rimane una domanda aperta, sebbene i modelli polinomiali confutino un relativo "miglioramento dell'equivalenza approssimata".

5. Significato

• Disaccoppiamento degli Assiomi: Il lavoro dimostra che la proprietà di "univalenza" di un universo può essere separata dalla proprietà di "estendibilità delle funzioni". Ciò sfida l'intuizione secondo cui l'univalenza è un assioma monolitico che forza tutti i principi di estendibilità.
• Intuizione Strutturale: Mostrando che l'Univalenza si fattorizza in Univalenza Categorical ed Estendibilità delle Funzioni, gli autori forniscono una comprensione strutturale più chiara di ciò che fa "funzionare" l'assioma di univalenza. Suggerisce che le funzioni sono "privilegiate" nella dichiarazione standard dell'univalenza specificamente a causa dell'interazione con FE.
• Teoria dei Modelli: Il lavoro convalida la costruzione del modello polinomiale come strumento potente per separare assiomi sottili nella teoria dei tipi, estendendone l'utilità oltre la semplice confutazione di FE all'analisi della struttura interna dell'univalenza.
• Implicazioni Fondazionali: Per i costruttivisti e i ricercatori fondazionali, ciò suggerisce che è possibile adottare una forma di univalenza (univalenza categoriale) che preserva l'equivalenza strutturale dei tipi senza impegnarsi nel principio più forte, storicamente difficile da integrare, dell'estendibilità delle funzioni.

In sintesi, il lavoro risolve la domanda di Dorais in senso negativo: l'Univalenza Categorical è strettamente più debole dell'Univalenza completa e non implica l'Estendibilità delle Funzioni.