Preuve-non-pertinence des types d'identité

Question

Dans les théories de type constructives, nous faisons une distinction entre les types d'identité extensionnelle et intensionelle. Il est trivial que les types d'identité extensifs ne soient pas pertinents pour la preuve, car l'habitant d'un type d'identité extensible est une constante$\textsf{eq}:\textsf{Eq}(a,b,A)$ (pour $a,b:A$ et $a=b:A$). En ce qui concerne les types d'identités intensionnelles, j'ai deux questions:

1. Laisser $A$ être un type arbitraire, est le type d'identité intensive $\textsf{Id}(a,b,A)$ (pour $a,b:A$ et $a=b:A$) preuve sans importance?

2. Laisser $A$ être un type non pertinent pour la preuve, est $\textsf{Id}(a,b,A)$ (pour $a,b:A$ et $a=b:A$) preuve sans importance?

Remarque: un type $A$ est considéré comme non pertinent pour la preuve ssi $A$ satisfait: $(\Pi x,y:A)\textsf{Id}(x,y,A)$.

Merci d'avance!

Answer 1

Soit 𝐴 un type arbitraire, le type d'identité intensionnelle 𝖨𝖽 (𝑎, 𝑏, 𝐴) (pour 𝑎, 𝑏: 𝐴 et 𝑎 = 𝑏: 𝐴) n'est-il pas pertinent pour la preuve?

Cela n'est ni prouvable ni réfutable dans la théorie des types intensifs. Vous pouvez l'ajouter comme axiome (unicité des preuves d'identité, UIP), ou ajouter des axiomes qui impliquent sa négation. La théorie des types extensionnels fait la première, la théorie des types d'homotopie la seconde. L'axiome d'univalence dans HoTT implique la négation de UIP.

Soit 𝐴 un type non pertinent pour la preuve, est-ce que 𝖨𝖽 (𝑎, 𝑏, 𝐴) (pour 𝑎, 𝑏: 𝐴 et 𝑎 = 𝑏: 𝐴) n'est pas pertinent pour la preuve?

Oui. Voir le lemme 3.3.4 dans le livre HoTT , ou le chapitre 7 pour un traitement plus général.

En général, les types ont des niveaux h, qui mesurent la quantité d'informations pertinentes dans les types d'identité. Niveau$0$ a des types équivalents au type d'unité et au niveau $(n+1)$a des types dont les types d'identité sont au niveau n. Dans le livre, les niveaux commencent à partir de$-2$ pour des raisons historiques, mais parfois les gens commencent $0$. Si un type est au niveau$n$, c'est aussi au niveau $(n + 1)$, donc son type d'identité est également au niveau $n$. Depuis être au niveau$1$ équivaut à n'être pas pertinent pour la preuve, un type non pertinent pour la preuve a des types d'identité non pertinents pour la preuve.

Ces résultats sur les niveaux h sont valables dans la théorie des types intensifs simples, sans aucune caractéristique spécifique à HoTT requise.