You can formulate the reflection rule in HoTT, postulating that every equality is in fact judgmental, But this implies that all the higher groupoid structure collapses, and hence is inconsistent with the univalence axiom.

In other words, if you want univalence-- if you want to treat isomorphisms on equal footing with equalities-- you _have to_ expand the definition of equality. You can think of univalence as saying that all equalities are "secretly" isomorphisms (strictly speaking, equivalences).