3

I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior version. Lots of attempts have been made previously to add extensionality features to type theory that have been missing relative to e.g. set theory, but they ...


3

I won't lie: I don't understand the homotopy part of homotopy type theory. But I have a decent grasp of Univalence, which is the axiom at the heart of Homotopy Type Theory (HoTT). The main idea of univalence is that we treat equivalences (essentially, isomorphisms) as equalities. When two types are isomorphic, you have a way to get from one to the other and ...


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 ...


1

Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a ...


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