3

Agda is definitely the better choice if you're doing Homotopy Type Theory. Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can ...


Only top voted, non community-wiki answers of a minimum length are eligible