<p><a href="https://github.com/fmota/hott">Here</a> is a small, incomplete, and <strong>inconsistent</strong> 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.</p>

<p><strong>Barrier 1:</strong>
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, <a href="https://github.com/fmota/hott/blob/master/bad.idr">we can easily prove</a> <code>True = False</code>.</p>

<p><strong>Barrier 2:</strong> 
The pattern matching in Idris is too strong for HoTT, as Neel Krishnaswami suspected in a comment above. <a href="https://github.com/fmota/hott/blob/master/k.idr">We can derive Streicher's K.</a> This leads to uniqueness of identity proofs, and is therefore incompatible with univalence. We can once again show <code>True = False</code>.</p>

CC BY-SA 3.0
2014-12-30T21:48:45.750Z
2014-12-31T00:52:37.910Z
2014-12-31T00:52:37.910Z
Francisco Mota
<p>Looking at the <a href="http://homotopytypetheory.org/">homotopy type theory blog</a> one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq. </p>

<p>Is there anyone aware if there is any similar attempt to formalize HoTT in <a href="http://www.idris-lang.org/">Idris</a>?</p>

CC BY-SA 3.0
2014-12-28T05:24:13.700Z
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).
Mike Shulman
CC BY-SA 3.0
2014-12-28T14:04:24.807Z
@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?
Giorgio Mossa
CC BY-SA 3.0
2014-12-28T19:38:30.533Z
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 `postulated`ed.
Andrej Bauer
CC BY-SA 3.0
2014-12-29T05:08:36.450Z
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.
Mike Shulman
CC BY-SA 3.0
2014-12-29T16:59:19.753Z
I have a small and incomplete formalization of HoTT in Idris. I'll post it up on Github later today.

Idris doesn't have a `postulate` or `axiom`, as far as I can tell, but you can introduce "metavariables" which correspond to values that have yet to be filled in. It's very easy to just have `univalence` be one such metavariable, and formalize everything around that.
Francisco Mota
CC BY-SA 3.0
2014-12-29T19:29:19.757Z
Just out of curiosity, why do you ask? The similarities between Agda and Idris are very strong, as you have noticed, so I'm curious what your motivation for working in Idris is.
cody
CC BY-SA 3.0
2014-12-30T12:11:18.223Z
@cody It's primarily a matter of curiousity, anyway I wanted to deepen the differences between these two languages.
Giorgio Mossa
CC BY-SA 3.0
2014-12-30T23:06:32.780Z
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.
Neel Krishnaswami
CC BY-SA 3.0
2014-12-31T00:43:38.803Z
@NeelKrishnaswami: Spot on! [I ran a little experiment.](https://github.com/fmota/hott/blob/master/k.idr) The pattern matching in Idris lets you prove K, even without heterogeneous equality. (Time to update my answer.)
Francisco Mota
<proof-assistants><homotopy-type-theory>
Formalizing Homotopy Type theory in Idris
Giorgio Mossa
# Formalizing Homotopy Type theory in Idris

(Asked by: username_0 on 2014-12-27)

Looking at the [homotopy type theory blog](http://homotopytypetheory.org/) 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](http://www.idris-lang.org/)?

**Tags:** proof-assistants, homotopy-type-theory
> **Comments:**
> **username_1**: 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).  
> **username_0**: @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?  
> **username_2**: 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 `postulated`ed.  
> **username_1**: 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.  
> **username_3**: I have a small and incomplete formalization of HoTT in Idris. I'll post it up on Github later today.  Idris doesn't have a `postulate` or `axiom`, as far as I can tell, but you can introduce "metavariables" which correspond to values that have yet to be filled in. It's very easy to just have `univalence` be one such metavariable, and formalize everything around that.  
> **username_4**: Just out of curiosity, why do you ask? The similarities between Agda and Idris are very strong, as you have noticed, so I'm curious what your motivation for working in Idris is.  
> **username_0**: @cody It's primarily a matter of curiousity, anyway I wanted to deepen the differences between these two languages.  
> **username_5**: 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.  
> **username_3**: @NeelKrishnaswami: Spot on! [I ran a little experiment.](https://github.com/fmota/hott/blob/master/k.idr) The pattern matching in Idris lets you prove K, even without heterogeneous equality. (Time to update my answer.)  

---

## 1 answers

### Answer by username_3 on 2014-12-30. Score: 21 | Accepted answer

[Here](https://github.com/fmota/hott) 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](https://github.com/fmota/hott/blob/master/bad.idr) `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.](https://github.com/fmota/hott/blob/master/k.idr) This leads to uniqueness of identity proofs, and is therefore incompatible with univalence. We can once again show `True = False`.


---

