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.

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.

Posting on behalf of Milli Maietti.

A foundation for constructive mathematics without unique choice is the

Minimalist Foundation (MF) ideated in

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

and completed in

http://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

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

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

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

as a generalization of the ex/lex completion.

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.