Strict proof-theoretic strength of the HIT real axiom

Let $\mathbf{MLTT}^-$ be Martin-Löf type theory without $W$-types, let $\mathbf{UA}$ denote the univalence axiom, and let $\mathbb{R}_{\mathbf{HIT}}$ denote the axiom that the higher-inductive Cauchy reals exist at the first universe level. HIT real strength conjecture. The theory

$$\mathbf{MLTT}^- + \mathbf{UA} + \mathbb{R}_{\mathbf{HIT}}$$

has strictly greater proof-theoretic strength than $\mathbf{MLTT}^-$. The comparison concerns whether the higher-inductive real axiom can be constructed in cubical sets within an absolutely predicative metatheory; establishing this would require an infinitary inductive definition unavailable in $\mathbf{MLTT}^-$.