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.
