 Solution

For ordinals, the inductive definition of ordinal addition isThe synthetic definition takes a well-order of type $\alpha$, followed by a disjoint well-order of type $\beta$, with every point of the first preceding the second. They agree by transfinite induction on $\beta$: the empty second order does nothing; adding its last point takes the successor; at a limit ordinal, the concatenated order is the union of its initial concatenations, whose types have the displayed supremum.