  A final remark: although constructive and intuitionistic set theories are compatible with the principles of choice just mentioned, the set theories are often defined without any choice principles. This has the aim of allowing for a “pluralistic” foundational approach. In particular, one would like to obtain a foundational theory compatible with those contexts (e.g. categorical models of set theory) in which even these weaker principles of choice may not be validated. For similar ideas in the context of constructive type theory, see (Maietti and Sambin 2005, Maietti 2009). We wish also to mention here Richman’s appeal for a constructive mathematics which makes no use of choice principles (Richman 2000; 2001).