Theoretical Computer Science
proof-assistants homotopy-type-theory
Updated Wed, 01 Jun 2022 01:42:03 GMT

Formalizing Homotopy Type theory in Idris

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?


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.