[gallabytes]

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