In the computer science literature I have seen cases in which they move from booleans to $\mathsf{Set}$ for obtaining a "proof-relevant" version of a concept (especially in formalisations).
As the booleans work like the subobject classifier of $\mathsf{Set}$, and in some sense it accounts for the truth values, I wonder if there is something like a topos in which $\mathsf{Set}$ itself (somehow, I don't know) is the subobject classifier, and if this gives a version of proof-relevant set theory?
I know it is a bit sketchy, but trying to formalise this I get lost by size problems.