@gadmm @MartinEscardo As martin said, Mac Lane and Moerdijk explain this. But in case it helps to give a shortcut: the topos theoretic interpretation of “element” is “singleton predicate”. Under this interpretation, the (proof relevant) double negation translation of type structure reduces to the usual (proof irrelevant) double negation translation of predicate structure.