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
and completed in
Maietti, A minimalist two-level foundation for constructive mathematics
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
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
as a generalization of the ex/lex completion.
