Solution (source code)

= Solution

For <ordinals>, the inductive definition of <ordinal addition> is
$$
\alpha+0=\alpha,\quad\alpha+(\beta+1)=(\alpha+\beta)+1,\quad
\alpha+\lambda=\sup_{\beta<\lambda}(\alpha+\beta)\quad(\lambda\text{ a nonzero limit ordinal}).
$$
The 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.