4 ms·
Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is unde
by rndn 11y ago
Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?
- gallabytes 11y agoWhy would it do that? Univalence is unrelated to the halting problem. What the univalence axiom says is that you can treat types you have proven isomorphic as equal.
- eli_gottlieb 11y agoNo. Homotopy Type Theory is a total language, so even type-level programming simply has to terminate, or the proof-checker won't accept it. Proving that nontrivially recursive programs terminate can be a bugger.
- jonsterling 11y agoYou do not in general decide whether two types are equivalent. You prove it...