 As is often the case in constructive mathematics generally, very simple notions of classical set theory (such as the notion of an ordinal) require careful reformulation to obtain the appropriate definition for the constructive environment (and the formulations often appear more complicated than familiar ones to the classical eye). Being inexpert, we will not involve ourselves further in this. It is worth noting that IZF, like many but not all constructive systems, admits a double negation interpretation of the corresponding classical theory ZF; we might think of IZF as a weakened version of ZF from the classical standpoint, but in its own terms it is the theory of a larger, more complex realm in which a copy of the classical universe of set theory is embedded.