Formalisierung der Homotopietypentheorie in Idris

Wenn man sich den Blog über Homotopietypentheorie ansieht , findet man leicht eine Menge Bibliotheken, die die meisten Homotopietypentheorien in Agda und Coq formalisieren.

Ist jemandem bekannt, ob es einen ähnlichen Versuch gibt, HoTT in Idris zu formalisieren ?

proof-assistants homotopy-type-theory Giorgio Mossa
quelle

Mir sind keine bekannt, und ich gehe davon aus, dass wir wahrscheinlich davon gehört hätten, wenn es jemand versucht hätte (oder zumindest, wenn es ihm gelungen wäre).

Mike Shulman

@MikeShulman Sollten die Typsysteme von Idris und Agda nicht im Wesentlichen gleichwertig sein? In diesem Fall sollte es möglich sein, HoTT auch in Idris zu formalisieren, oder?

Giorgio Mossa

Idris ist stärker auf Programmierung ausgerichtet. Eine Sache, die mich beunruhigen würde, ist, ob es das Äquivalent von Agda postulateoder Coq hat Axiom. Wenn ja, wie schafft es das, damit zu rechnen (es ist eine kompilierte Sprache)? Der Punkt ist, dass das Univalenz-Axiom herausgearbeitet werden muss postulated.

Andrej Bauer

Ich wollte mit Sicherheit nicht sagen, dass ich das nicht für möglich halte! Ich kenne nur niemanden, der es schon versucht hat. Ich weiß so gut wie nichts über Idris.

Mike Shulman

Ich gehe davon aus, dass Sie mit Idris das K-Axiom (Eindeutigkeit von Identitätsnachweisen) von Streicher durch Pattern Matching (wie Agda es bis vor kurzem getan hat) beweisen können, was für HoTT ein Problem darstellen würde.

Neel Krishnaswami

Antworten:

Hier ist eine kleine, unvollständige und inkonsistente Formalisierung von HoTT in Idris. Es zeigt, dass Sie einen Widerspruch in Idris nur herleiten können, indem Sie Univalenz postulieren. Momentan gibt es zwei Hindernisse für die Formalisierung von HoTT in Idris.

\prod_{P : X \to T y p e} \prod_{x : X} \prod_{p : x = x} \prod_{a, b : P x} (t r a n s p o r t P p a = b) \to (a = 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

Barriere 2: Die Musterübereinstimmung in Idris ist für HoTT zu stark, wie Neel Krishnaswami in einem obigen Kommentar vermutet hat. Wir können Streichers K ableiten. Dies führt zur Eindeutigkeit von Identitätsnachweisen und ist daher mit der Univalenz unvereinbar. Wir können noch einmal zeigen True = False.

Francisco Mota
quelle