Fondamenti di Teoria Omotopica dei Tipi

La teoria omotopica dei tipi, come suggerisce il nome, non è altro che una branca della teoria dei tipi. La teoria dei tipi può svolgere il ruolo di teoria fondazionale della matematica. Infatti le principali applicazioni della teoria dei tipi in ambito matematico sono nello sviluppo dei proof assistant. I proof assistant sono software che normalmente constano di due parti: un linguaggio e un type checker. Il linguaggio non è altro che una grammatica generativa in cui vengono scritte le dimostrazioni matematiche. Il type checker verifica poi che ogni passaggio sia corretto rispetto al sistema formale. Se il type checking ha esito positivo allora il risultato può essere considerato dimostrato e convalidato. Il vantaggio di questo approccio è che il type checker fornisce un grado di sicurezza maggiore della verifica umana. L'ostacolo pratico principale deriva dalla laboriosità nella stesura esplicita delle dimostrazioni. In questo senso la teoria ZF risulta completamente inadeguata: anche un teorema banale presenta troppe complicazioni tecniche. Intuitivamente, la struttura di insieme codifica l'informazione matematica sotto forma di gerarchia. Decodificare l'informazione è dispendioso perché comporta una laboriosa esplorazione di tale struttura gerarchica. La teoria delle categorie invece presenta un problema differente: non si presta ad essere ben formulata in un sistema formale. Le teorie dei tipi invece si esprimono facilmente sotto forma di sistema formale e ogni teoria dei tipi cerca in qualche modo di semplificare la stesura esplicita delle dimostrazioni. Dunque sorge spontanea la domanda: quale attività viene resa più agevole nella teoria omotopica dei tipi rispetto alle altre teorie dei tipi? Tutto ruota attorno all'Assioma di Univalenza. Formulato da Voevodsky, è il principale suo contributo alla teoria dei tipi. Si consideri la diffusa pratica matematica di considerare uguali strutture isomorfe. Se dimostriamo un teorema per la struttura M e M è isomorfo ad N, in realtà ridimostrare il teorema per N può richiedere numerosi passaggi tecnici, ciò è dispendio di energie e tempo e non apporta nessun contributo significativo alla matematica. La teoria omotopica dei tipi risolve questo con l'Assioma di Univalenza: strutture isomorfe sono uguali. Dunque non c'è bisogno di riscrivere la dimostrazione. La teoria omotopica dei tipi può essere riassunta come: una teoria dei tipi con tipi dipendenti, intuizionista (di Per Martin-Löf), intensionale e proof-relevant a cui viene aggiunto l'Assioma di Univalenza.