basic constructions:
strong axioms
Barr’s theorem states: If a statement in geometric logic is deducible from a geometric theory using classical logic and the axiom of choice, then it is also deducible from it in constructive mathematics.
The proof of Barr’s theorem itself, however, is highly non-constructive.
If $\mathcal{E}$ is a Grothendieck topos, then there is a surjective geometric morphism
where $\mathcal{F}$ satisfies the axiom of choice.
See
for a discussion of the importance of this theorem in constructive algebra.