16
$\begingroup$

Looking at the homotopy type theory blog one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq.

Is there anyone aware if there is any similar attempt to formalize HoTT in Idris?

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ I'm not aware of any, and I expect we probably would have heard about it if anyone had tried (or at least if they had succeeded). $\endgroup$ – Mike Shulman Dec 28 '14 at 5:24
  • $\begingroup$ @MikeShulman Shouldn't Idris and Agda's type systems be essentially equivalent? In that case it should be possibile to formalize HoTT in Idris too, shouldn't it? $\endgroup$ – Giorgio Mossa Dec 28 '14 at 14:04
  • $\begingroup$ Idris is oriented more heavily towards programming. One thing that would worry me is whether it has the equivalent of Agda postulate or Coq Axiom. If it does, how does it manage to compute with it (it's a compiled language)? The point is that the univalence axiom needs to be postulateded. $\endgroup$ – Andrej Bauer Dec 28 '14 at 19:38
  • $\begingroup$ I certainly didn't mean to say I didn't think it would be possible! I just don't know of anyone that has tried it yet. I know next to nothing about Idris. $\endgroup$ – Mike Shulman Dec 29 '14 at 5:08
  • 4
    $\begingroup$ I expect Idris lets you prove the Streicher's K axiom (uniqueness of identity proofs) via pattern matching (as Agda did until recently), which would be a problem for HoTT. $\endgroup$ – Neel Krishnaswami Dec 30 '14 at 23:06
19
$\begingroup$

Here is a small, incomplete, and inconsistent formalization of HoTT in Idris. It shows that you can derive a contradiction in Idris just by postulating univalence. There are two barriers to formalizing HoTT in Idris at the moment.

Barrier 1: Idris has heterogeneous equality and heterogeneous equality rewriting. From the HoTT perspective this means we have access to the following rewriting principle, which is inconsistent with univalence: $$ \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) $$ With this principle, we can easily prove True = False.

Barrier 2: The pattern matching in Idris is too strong for HoTT, as Neel Krishnaswami suspected in a comment above. We can derive Streicher's K. This leads to uniqueness of identity proofs, and is therefore incompatible with univalence. We can once again show True = False.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.