  As we have seen, implementing mathematical objects (ZF-style) as wellfounded sets and then reasoning about those wellfounded sets) is not a very satisfactory way to proceed, since NF does not have sufficient strength for us to manipulate the implemented objects with the freedom we want. The situation with the endogenous interpretation (mathematical objects as global equivalence classes) is potentially more satisfactory. In this scenario cardinals are implemented as equivalence classes under equipollence and are (big) sets. The collection of all cardinals is a set. Ordinals can be handled similarly: ordinals are (big) sets and the collection of all ordinals is a (big) set; the collection of all groups is a set, the collection of all rings is a set; …. Being big, these sets cannot be manipulated in the freewheeling way that small sets can be. (The axiom of scheme of (full, unstratified) separation fails for big sets: if it didn’t then the Russell class would be \(\{x \in V: x \not\in x\})\) and their manipulation is complicated by the appearance on the scene of various analogues of the \(T\) function (that we saw in connection with the cardinals) that are needed to work round the stratification constraints. However, it is most striking that this doesn’t turn out to be much of a problem. On the whole, ordinary mathematics seems to be what the Computer Scientists call strongly typed, and to a large extent the stratification constraints of NF coincide with the endogenous strong typing of the mathematical objects being implemented. Sadly there is no space here for a proper discussion of this deep and interesting question.