@JoelDavidHamkins You could use weaker universe concepts in HoTT. A universe which is closed under identity types, dependent sum types, and natural numbers, but not dependent product types, corresponds to the regular cardinals in set theory.

There is an axiom of replacement in type theory which specifically applies to universes. It is used in Egbert Rijke's textbook on HoTT to construct quotient sets. Replacement also follows from certain higher inductive types such as homotopy pushouts.

Never mind, I got the wrong axiom, it's $AC_{00}$ rather than weak countable choice which makes the two notions of real numbers the same.

Speaking of which, I highly suspect that one only needs weak countable choice rather than countable choice in order to prove that IVT and the analytic LLPO are logically equivalent.

Ah, it's the Dedekind real numbers. This means that you are talking about the analytic LLPO, which is stronger than the traditional LLPO for natural numbers, but becomes logically equivalent to the latter with weak countable choice.

What definition of the real numbers are you using? The definition via Cauchy sequences of rationals? The definition via two-sided Dedekind cuts?

@saolof the "real numbers" used in smooth topoi are only a local ring, because if they were a Heyting field, then one could prove that equality is stable with respect to double negation, (because given a proposition $P$, $\neg \neg \neg P$ implies $\neg P$, and in a Heyting field, the negation of apartness is equality), and thus every element which is not not equal to zero is equal to zero.