The equality in the title of this post is just the injectivity of type constructors, which, just like injectivity of term level constructors, seems very trivial to me.
That is the key assumption that needs to be substantiated. It is not actually obvious that type constructors ought to be injective, and univalence is a prime example of a reasoning principle that it contradicts.
In Haskell and OCaml, the injectivity of type constructors helps type inference, but that is a rather narrow way to look at it. More semantic interpretations of types, where types are not just labels on terms to prevent mistakes, but explicitly describe how terms “behave”, can make injectivity much harder or impossible to justify.
I really cannot see why this would be inconsistent with any reasonable proof system.
Even if it were the case that injectivity of type constructor did not contradict any worthwhile system, there may still be a cost to adding it to a particular system. In Coq,
= is not a primitive of the system, it is user-defined, subject to much more fundamental rules. Slapping axioms on top arbitrarily is bound to make it more difficult to ensure the well-behavedness of the system. In that sense, injectivity of type constructors is not actually obvious.
It’s certainly feasible to live without it, although it might take some effort getting accustomed to it.