9

it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer My understanding is that it matches points of path rather than path itself. This is why the matching is on posneg x (where x : I) rather than posneg itself. Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a ...


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