In set theory, the axiom of dependent choice (DC) states that if is a nonempty (inhabited) set and if is a total binary relation on , then there exists a sequence such that belongs to for all . It is strictly weaker than the full axiom of choice, but strictly stronger than the axiom of countable choice. It is called dependent choice because the available choices for depend on the choice of made at the previous stage.
For a number of schools of constructive mathematics, dependent choice is considered an acceptable alternative to full AC, and the principle holds (assuming that it holds in Set) in quite a few toposes of interest in which full AC doesn’t hold, including all presheaf toposes and the effective topos. In fact, it follows from the stronger presentation axiom, which holds in many of these toposes and also has a constructive justification.