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

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.