Formalisation de la théorie du type d'homotopie dans Idris

En regardant le blog sur la théorie des types d'homotopie, on peut facilement trouver beaucoup de bibliothèque formalisant la plupart de la théorie des types d'homotopie dans Agda et Coq.

Quelqu'un sait-il s'il existe une tentative similaire de formaliser HoTT dans Idris ?

proof-assistants homotopy-type-theory Giorgio Mossa
la source

Je n'en connais aucun, et je pense que nous en aurions probablement entendu parler si quelqu'un avait essayé (ou du moins s'il avait réussi).

Mike Shulman

@MikeShulman Les systèmes de type d'Idris et d'Agda ne devraient-ils pas être essentiellement équivalents? Dans ce cas, il devrait également être possible de formaliser HoTT dans Idris, n'est-ce pas?

Giorgio Mossa

Idris est davantage orienté vers la programmation. Une chose qui m'inquiéterait est de savoir si elle a l'équivalent d'Agda postulateou de Coq Axiom. Si c'est le cas, comment parvient-il à calculer avec lui (c'est un langage compilé)? Le fait est que l'axiome d'univalence doit être postulatedédité.

Andrej Bauer

Je ne voulais certainement pas dire que je ne pensais pas que ce serait possible! Je ne connais personne qui l'ait encore essayé. Je ne sais presque rien d'Idris.

Mike Shulman

Je pense qu'Idris vous permet de prouver l'axiome K de Streicher (unicité des preuves d'identité) via la correspondance de modèles (comme Agda l'a fait jusqu'à récemment), ce qui serait un problème pour HoTT.

Neel Krishnaswami

Réponses:

Voici une petite formalisation incomplète et incohérente de HoTT dans Idris. Cela montre que vous pouvez dériver une contradiction dans Idris simplement en postulant l'univalence. Il existe actuellement deux obstacles à la formalisation de HoTT dans Idris.

Obstacle 1: Idris a une réécriture d'égalité hétérogène et d'égalité hétérogène. Du point de vue de HoTT, cela signifie que nous avons accès au principe de réécriture suivant, qui est incompatible avec l'univalence: ,: Avec ce principe, nous pouvons facilement prouver .

\prod_{P : X \to T y p e} \prod_{X : X} \prod_{p : X = X} \prod_{une, b : P X} (t r une n s p o r t P p une = b) \to (une = b)

$\prod_{P \,:\, X \to \mathsf{Type}}\ \prod_{x\,:\,X}\ \prod_{p \,:\, x = x}\ \prod_{a,\,b \,:\, P\, x} (\mathsf{transport}\ P\ p\ a = b) \to (a = b)$ True = False

Obstacle 2: La correspondance de motifs dans Idris est trop forte pour HoTT, comme le suspectait Neel Krishnaswami dans un commentaire ci-dessus. Nous pouvons dériver le K. de Streicher. Cela conduit à l'unicité des preuves d'identité, et est donc incompatible avec l'univalence. Nous pouvons à nouveau montrer True = False.

Francisco Mota
la source