Prova di irrilevanza dei tipi di identità
Nelle teorie dei tipi costruttivi, facciamo una distinzione tra tipi di identità estensionale e intensionale. È banale che i tipi di identità estensionale siano prove irrilevanti poiché l'abitante di un tipo di identità estensionale è una costante$\textsf{eq}:\textsf{Eq}(a,b,A)$ (per $a,b:A$ e $a=b:A$). Per quanto riguarda i tipi di identità intensionali, ho due domande:
Permettere $A$ essere un tipo arbitrario, è il tipo di identità intensionale $\textsf{Id}(a,b,A)$ (per $a,b:A$ e $a=b:A$) prova irrilevante?
Permettere $A$ essere un tipo irrilevante per la prova, è $\textsf{Id}(a,b,A)$ (per $a,b:A$ e $a=b:A$) prova irrilevante?
Nota: un tipo $A$ si dice che sia irrilevante per la prova iff $A$ soddisfa: $(\Pi x,y:A)\textsf{Id}(x,y,A)$.
Grazie in anticipo!
Risposte
Sia 𝐴 un tipo arbitrario, il tipo di identità intensionale 𝖨𝖽 (𝑎, 𝑏, 𝐴) (per 𝑎, 𝑏: 𝐴 e 𝑎 = 𝑏: 𝐴) prova irrilevante?
Questo non è dimostrabile o dimostrabile nella teoria dei tipi intensionali. Puoi aggiungerlo come assioma (unicità delle prove di identità, UIP) o aggiungere assiomi che implicano la sua negazione. La teoria dei tipi estensionale fa la prima, la teoria dei tipi di omotopia la seconda. L'assioma di univalenza in HoTT implica la negazione dell'UIP.
Sia 𝐴 un tipo irrilevante per la prova, 𝖨𝖽 (𝑎, 𝑏, 𝐴) (per 𝑎, 𝑏: 𝐴 e 𝑎 = 𝑏: 𝐴) è irrilevante per la prova?
Sì. Vedere il Lemma 3.3.4 nel libro HoTT o il Capitolo 7 per una trattazione più generale.
In generale, i tipi hanno livelli h, che misurano la quantità di informazioni rilevanti nei tipi di identità. Livello$0$ ha tipi che sono equivalenti al tipo di unità e al livello $(n+1)$ha tipi i cui tipi di identità sono al livello n. Nel libro, i livelli iniziano da$-2$ per ragioni storiche, ma a volte le persone partono da $0$. Se un tipo è a livello$n$, è anche a livello $(n + 1)$, quindi anche il suo tipo di identità è a livello $n$. Da quando sei a livello$1$ è lo stesso che essere irrilevante per la prova, un tipo irrilevante per la prova ha tipi di identità irrilevanti per la prova.
Questi risultati sui livelli h si mantengono nella semplice teoria dei tipi intensionali, senza che siano richieste caratteristiche specifiche di HoTT.