Posting on behalf of Milli Maietti. 

A foundation for constructive mathematics  without unique choice is the

Minimalist Foundation (MF) ideated in

https://www.math.unipd.it/~maietti/papers/MaiettiSambin-rev2.pdf

and completed in

https://www.math.unipd.it/~maietti/papers/tt.pdf

This is meant as a  base system to formalize constructive point-free topology and perform constructive reverse mathematics,
where

- Dedekind reals  and Cauchy reals  defined in terms of functional relations do not form a set

(only Cauchy type-theoretic reals do form a set),
even in the *classical extension* of MF with excluded middle
as explained in

https://www.math.unipd.it/~maietti/papers/whyp.pdf


A quotient completion of a tripos which does not impose unique choice
has been introduced in

https://www.math.unipd.it/~maietti/papers/quLU.pdf

as a generalization of the ex/lex completion.