In classical mathematics, ordinal arithmetic is well-studied; constructively, addition and multiplication are well-known. We study constructive ordinal exponentiation, where ordinals are taken to be transitive, extensional, and wellfounded orders on sets. We present a negative result showing that general constructive ordinal exponentiation is impossible, but we suggest two definitions that come close. The first definition is abstract and solely motivated by the expected equations; this works as long as the base of the exponential is positive. The second definition is based on decreasing lists and can be seen as a constructive version of Sierpi{ń}ski's definition via functions with finite support; this requires the base to have a trichotomous least element. Whenever it makes sense to ask the question, the two constructions are equivalent, allowing us to prove algebraic laws, cancellation properties, and preservation of decidability of the exponential. The core ideas do not depend on any specific constructive set theory or type theory, but a concrete computer-checked mechanization using the Agda proof assistant is given in homotopy type theory.

翻译：暂无翻译