A trick that faithfully embeds any Grothendieck topos into one that satisfies the axiom of choice. (“Barr’s theorem”)
nLab page on Boolean localisation