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$ Commented Dec 28, 2014 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$ Commented Dec 28, 2014 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$ Commented Dec 28, 2014 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$ Commented Dec 29, 2014 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$ Commented Dec 30, 2014 at 23:06

1 Answer 1


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 and acknowledge you have read our privacy policy.

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