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

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