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

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`

.

External links referenced by this document: