4 ms·
Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence.
by TheAsprngHacker 7y ago
Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence. In vanilla MLTT, a = b is inhabited iff a and b share the same normal form, and its proof is refl (reflexivity). In HoTT, a = b may be inhabited by proofs other than refl. Namely, the univalence axiom states that types are equal when they are isomorphic, and function extensionality states that functions are equal when they map the same inputs to the same outputs. You also get higher inductive types, which allow you to define constructors of equalities on inductive types. So, HoTT allows you to prove things that you can't prove under ordinary MLTT.
- pron 7y ago> So, HoTT allows you to prove things that you can't prove under ordinary MLTT. Well, adding consistent axioms often allows proving more thing, but that in itself does not necessarily mean it's more useful, and certainly not that proofs are easier -- that, I believe, was the question. For example, adding the axiom 1/0 = 0 is consistent with ordinary arithmetics, and also allows you to prove more things (e.g. that 1/0 = 0), but is not necessarily useful and not necessarily helpful.