The standard definition of the cumulative hierarchy in first-order ZF is based on transfinite recursion on ordinals. Hence the construction involves at least a profound ordinal theory and appears rather late in a description of ZF. In a higher order logic such as classical type theory, the cumulative hierarchy can be characterized by inductive definitions building on an axiomatized type of sets. During a three-month research immersion lab (RIL), we investigated this alternative approach resulting in the common relations between ordinals, cumulative sets and well-founded sets. Of related interest were the general study of well-orderings and isomorphisms on type level.