Defining stuff in:
* type theory: uh, just remember to define everything in order?
* "classical mathematics": so we need these three sets, the first one can be arbitrary, but it's choice impacts how you pick the second one, while the third one has to be picked in the light of the full moon on the last Thursday of a month unless...