In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields.

CZF can still prove that there are dedekind reals, and that they are cauchy complete, but intersecting all of its cauchy complete subfields is impredicative (i.e. CZF doesn't have the powerset axiom). Also keep in mind that, without countable choice, you can't prove the cauchy reals are cauchy complete (but if they were they'd be minimal).

So, can CZF prove that there is a minimal extension of the rationals that is cauchy complete?

Another approach I thought of is taking the set of dedekind reals that can be formed using a well founded tree of cauchy sequences whose leaves are rational numbers. But I'm pretty sure the property of being a well founded tree has unbounded quantifiers, so we can't form a subset using it.

A set that I think is minimal is if we take the set of trees as above, but instead of requiring it to be well founded, we just require that the values at the nodes are determined by the leaves (i.e. for every other tree that has the same structure and leaves, it will also have the same internal nodes). But I couldn't figure out how to prove that this gives the minimal subfield we are looking for.