> A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means

> A consequence of HOT in relation to programs is that you can compare programs for equality without running them. I rediscovered this a few years ago. It means that e.g. certain physical simulations could be known to not complete without running them to assumed termination. Currently we are wasting millions of dollars running simulations that we could show will not produce valid results. I'm curious where you got this idea. Even if you express programs in HoTT so that equality of these programs corresponds to (say) identical outputs, there's no reason that this equality should be decidable any more than it is in ordinary mathematics. You might be confused by the fact that HoTT is (by default) constructive, but just because you can define something in HoTT does not mean that its equality is decidable. In fact, that's a defining property of constructivity in this context: if every type has decidable equality, then the law of excluded middle holds. The proof isn't too hard: simply apply the decidability of equality to the type of propositions and for a given proposition P, check if P = True is true or false. > systems where you do not accept the axiom of choice or, more interestingly, disregard it entirely. I'm wondering what the difference between those two is. "not accept" and "disregard" are synonyms to me, but maybe you have something more precise in mind. There's a distinction between not accepting an axiom (so that you're agnostic on the question of whether it holds) and accepting its negation. Maybe that's what you're thinking of. > it means real numbers "do not exist" as you can not write them down. In light of your other comment, I'd phrase this as "there are particular real numbers that don't exist" or "some real numbers don't exist". As written, it reads as if the set of real numbers doesn't exist. Even so, keep in mind the difference between not being able to prove something and being able to prove its negation. HoTT is consistent with adding in more axioms (as you alluded to above) which do imply that Chaitin's constant exists. So that means that the base theory can't prove that such constants don't exist (unless the base theory is inconsistent).