A form of {\mathrm {PEM}} corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any coequalizer of two nonintersecting monomorphisms has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically.
