Is it possible in constructive mathematics (no excluded middle or Axiom of Choice) to construct the algebraic numbers directly from the rationals (in say HoTT), without first constructing a real line and then augmenting it with the imaginary unit? In classical mathematics one could do this by appealing to the (obviously nonconstructive) principle that every field admits an algebraic closure.
One reason that I ask is that in constructive mathematics the real line seems a bit messy: the various constructions of the real line (Cauchy vs. Dedekind) are in general inequivalent without at least assuming countable choice, and in particular the usual construction of the Cauchy reals may not even be sequentially complete without countable choice (though the new higher-inductive type definition given in HoTT avoids this problem).
I'm relatively new to constructive mathematics, so I apologize if this construction is obvious (or obviously not possible).
Edit: I'm also curious about the constructive properties of the algebraic numbers, such as if they inherit decidable equality from the rationals?