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.
What the univalence axiom says is that you can treat types you have proven isomorphic as equal.
No comments yet.