nLab
Barr's theorem

Idea

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.

Statement

Theorem

If $ℰ$ is a Grothendieck topos, then there is a surjective geometric morphism

$$ℱ\to ℰ$$\mathcal{F} \to \mathcal{E}

where $ℱ$ satisfies the axiom of choice.

References

See

• Gavin Wraith, Intuitionistic algebra: some recent developments in topos theory In Proceedings of the International Congress of Mathematicians (Helsinki, 1978), pages 331–337, Helsinki, 1980. Acad. Sci. Fennica (pdf)

for a discussion of the importance of this theorem in constructive algebra.