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?

  • 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$ 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$ 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$ 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$ Dec 29 '14 at 5:08
  • 5
    $\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$ Dec 30 '14 at 23:06

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.


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.