Doesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?
Proving that nontrivially recursive programs terminate can be a bugger.
What the univalence axiom says is that you can treat types you have proven isomorphic as equal.