We’ll give two definitions, starting with the inductive: Definition (inductive) We define by recursion on (with fixed): where is a limit Definition (synthetic) We define to be the Order Type of (Cartesian Product of Well Ordered Sets) Properties provided