Background for the curious reader:
An ordinal $\beta$ is a transitive set in the sense that $\alpha\in\beta$ implies $\alpha\subset\beta$. Any ordinal is naturally well-ordered under $\in$ (so any subset of it has a least element), and any well-order is isomorphic to an ordinal. In fact, any class (naively, collection) of ordinals is itself well-ordered under the relation $\in$. This fact allows for the usage of transfinite induction and transfinite recursion.
We have three types of ordinals: the empty set $0=\emptyset=\{\; \}$, successor ordinals $S(\alpha)=\alpha\cup\{\alpha\}$ where $\alpha$ is an ordinal, and limit ordinals, which are all the other ones. Finite ordinals are either $0$ or successors, the set $\omega=\{0,1,2,\dots\}$ is a limit ordinal. A limit ordinal $\alpha$ has the property that $\alpha=\sup_{\beta<\alpha}\{\beta\}=\bigcup_{\beta<\alpha}\beta$.
My question
Ordinal arithmetic can be defined recursively as follows:
- $\alpha+0=\alpha$, $\alpha+S(\beta)=S(\alpha+\beta)$, $\alpha+\sup_{\gamma<\beta}\{\gamma\}=\sup_{\gamma<\beta}\{\alpha+\gamma\}$;
- $\alpha\cdot0=\alpha$, $\alpha\cdot S(\beta)=\alpha\cdot\beta+\alpha$, $\alpha\cdot\sup_{\gamma<\beta}\{\gamma\}=\sup_{\gamma<\beta}\{\alpha\cdot\gamma\}$;
- $\alpha^0=1$, $\alpha^{S(\beta)}=\alpha^\beta\cdot\alpha$, $\alpha^{\sup_{\gamma<\beta}\{\gamma\}}=\sup_{\gamma<\beta}\{\alpha^\gamma\}$.
Alternatively, one can define:
- $\alpha+\beta$ is the unique ordinal isomorphic to the disjoint union $\{0\}\times\alpha\cup\{1\}\times\beta$ given the lexicographic order.
- $\alpha\cdot\beta$ is the unique ordinal isomorphic to the Cartesian product $\beta\times\alpha$ given the lexicographic order.
As the disjoint union and Cartesian product are simply the categorical coproduct and the categorical product, I wonder if there is some way to actually categorify these alternate definitions. Additionally, I am not aware of any non-recursive version of exponentiation, so I would be curious if a categorical formulation of addition and product of ordinals also allows for a categorical (hence non-recursive) formulation of exponentiation.