Posting on behalf of Milli Maietti. 

A foundation for constructive mathematics  without unique choice is the Minimalist Foundation (MF) ideated in

[Maietti, Sambin, *Towards a minimalist foundation for constructive mathematics*](https://www.math.unipd.it/~maietti/papers/MaiettiSambin-rev2.pdf)

and completed in

[Maietti, *A minimalist two-level foundation for constructive mathematics*](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

[Maietti, Sambin, *Why topology in the minimalist foundation must be pointfree*](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

[Maietti, Rosolini, *Quotient completion for the foundation of constructive mathematics*](https://www.math.unipd.it/~maietti/papers/quLU.pdf)

as a generalization of the ex/lex completion.