At least in papers on cubical type theory, 'respecting equivalence' is somewhat independent of universes. There is a judgmental notion of paths:
$$Γ,i ⊢ T\ \mathsf{type} \\ Γ,i ⊢ t : T$$
The top being a 'type path' and the bottom being a 'term path'. Because these are judgments, you can't work with them as hypotheses exactly. But there are derived constructions like:
$$\frac{Γ,i⊢T\ \mathsf{type}\qquad Γ⊢ t_0 : T[i := 0]}{Γ ⊢ \mathsf{transport}_i\ T\ t_0 : T[i := 1]}$$
So, if you can judge that a path exists in types, then you can transport by it. Further, the $\mathsf{Glue}$ type (or whatever equivalent is used) lets you judge that a path exists based only on an equivalence. Something like (using $\mathsf{V}$ because it's simpler than $\mathsf{Glue}$):
$$\frac{Γ ⊢ e : Σ_{f : A → B}\ \mathsf{isEquiv}\ f}{Γ,i ⊢ \mathsf{V}_i\ e\ \ \mathsf{type}}$$
If you have a type path judgment, you can also abstract paths over it, I believe. So:
$$\frac{Γ,i ⊢ P\ \mathsf{type}\quad Γ ⊢ x : P[i := 0]\quad Γ ⊢ y : P[i := 1]}{Γ ⊢ \mathsf{Path}_{i. P}\ x\ y\ \mathsf{type}}$$
Note that none of this requires knowing that $A$ and $B$ belong to a common universe. If we can judge that $A$ and $B$ are types, we can judge that the type of $e$ is a valid type, build values, judge that $\mathsf{V}$ is a valid type (path), and transport through it. Judgmental rules say that $\mathsf{V}_0\ e = A$ and $\mathsf{V}_1\ e = B$. And we can talk about the type of values related by that path. In some sense, this is building univalence, "for all types," not just for a universe, although perhaps you could imagine that "all types" form a very large, implicit universe of sorts.
Now, strictly speaking, Agda doesn't work this way. It doesn't really have this 'judgment of types' prior to the classification of types by a universe. Rather, it is designed around the idea that every type has an intrinsic universe, and there are enough universes that you can get away with never talking about the $\mathsf{type}$ judgment directly, as a user. However, this means that all of the above stuff gets parameterized by a universe in Agda, and you are back to the univalent universe scenario, because $\mathsf{type}$ gets replaced with $: \mathsf{Type}_n$, and there's no way for $n$ to vary with $i$ (universes of different levels are not equivalent). I'm also not familiar with any comparable proof assistant (like, based in something resembling MLTT) that doesn't work this way, although I'm far from having tried everything.
So this can be seen as a point in favor of not structuring around a fixed hierarchy of universes, and instead letting universes be incidental reflections of parts of the totality of types. There are still some things that can't be spoken about without identifying a universe to work in (unless you add other features that aren't even present in most paper presentations of type theory). But it at least changes, "equivalence between types is respected if they belong to a common univalent universe," into something more like, "a universe is univalent if equality of its codes reflects the path judgment of the decodings."
On the flip side, you actually can try out this strategy in Agda by ignoring its universe hierarchy and polymorphism, and just working in $\mathsf{Type}_0$. Because that universe is closed under (higher) induction-recursion, you can introduce (univalent) universes internal to it, and the cubical machinery on $\mathsf{Type}_0$ works like the judgmental presentation in papers. Essentially $\mathsf{Type}_0$ is a model of (something like) the paper theory. I'm not familiar with what sort of tooling people imagine using with this sort of 'a la carte' universe classification, though, so it might get tedious for complicated situations due to a lack of such features in Agda.
So, on the one hand, you could say that Agda's (and others') design is lacking in certain ways. On the other hand, it has a feature (that seems often viewed with suspicion, and goes unused) that makes a small subtheory of it into a model of the 'improved' design that people would typically use, and you could try it out today.
I guess I'm uncertain if this answers your exact questions. Agda's universe polymorphism is an example of something that's actually very tedious to model using induction-recursion. I think the hope is that you could instead think less about universe 'arithmetic' in favor of always conjuring up the exact 'universe that pertains to this problem.' And then $\mathsf{Type}_0$ or the $\mathsf{type}$ judgment is the universe of everything anyone could possibly want to talk about, and everything defined on it is invariant under equivalence. So in that sense, it hopefully answers your question in the affirmative.
Addendum: here's an example of the sort of thing you can do. Suppose we have a type $L$ of levels, and a bunch of universes:
$$\mathsf{U} : L → \mathsf{Type}_0 \\ \mathsf{El} : \prod_{\ell:L} \mathsf{U}_\ell → \mathsf{Type}_0$$
Then we can define their union as a HIT:
module _
(L : Type)
(U : L → Type)
(El : ∀{ℓ} → U ℓ → Type)
where
variable
ℓ : L
s t : U ℓ
data ⋃U : Type where
ι : U ℓ → ⋃U
un : El s ≃ El t → ι s ≡ ι t
⋃El : ⋃U → Type
⋃El (ι x) = El x
⋃El (un e i) = ua e i
It doesn't really matter whether $\mathsf{U}_\ell$ was univalent, because we are imposing univalence on $\bigcup\!\mathsf{U}$. But at the same time, we are ensuring that families with type $\bigcup\!\mathsf{U} → \mathsf{Type}_0$ are defined in a more 'parametric' way. You can't just look at the $L$ values and do something different based on them, because you have to give equivalent answers for equivalent types regardless of which $\mathsf{U}_\ell$ they came from. Presumably it's not as parametric as not being able to inspect the values at all, but I'm not sure it's possible to do much better without more language features.
Anyhow, if we imagine that $F : \bigcup\!\mathsf{U} → \mathsf{Type}_0$ is a 'universe polymorphic' family, we can write the following:
inst : (⋃U → Type) → U ℓ → Type
inst F = F ∘ ι
lemma : (F : ⋃U → Type) → El s ≃ El t → inst F s ≡ inst F t
lemma F e = cong F (un e)
i.e. $\mathsf{inst}$ instantiates the polymorphic family to one of the universes, and if we apply the family to equivalent types, even in distinct universes, we can transport between the results.
If you want to decouple the level from the type, instead of packing them together like this example, and say that a definition in Agda with type like $(\ell : \mathsf{Level}) → \mathsf{Type}_\ell → ...$ satisfies an analogous property, then presumably you need something more like parametricity about $\mathsf{Level}$. This is because levels of distinct universes can't just be equal/have a path between them (or the universes would be equivalent), so there needs to be some looser sort of 'connection' between universe levels that, when combined with a Π type over $\mathsf{Level}$, yields the desired 'univalence across levels' principle.
liftis the identity? $\endgroup$