Formalizing Homotopy Type theory in Idris

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.

Solved by user7577 (633 )
Dec 30, 2014 at 21:48