Could not include topos theory - contents
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.
where satisfies the axiom of choice.
for a discussion of the importance of this theorem in constructive algebra.