一句话：在同伦类型论中给出构造性序数指数的两种定义，证明其等价并形式化验证代数律与可判定性。
本文研究构造性序数指数运算。作者将序数视为集合上传递、外延且良基的序关系，在同伦类型论框架下提出两种看似不同的定义：一种抽象定义通过序数的上确界给出，仅由期望满足的等式驱动；另一种具体定义基于递减列表，可视为 Sierpiński 以有限支撑函数为基础的经典构造的构造性版本。作者证明这两种方法在问题有意义时等价，并利用该等价证明指数运算的代数律与可判定性性质。全部结果均在证明助手 Agda 中形式化，展示了同伦类型论与机器化证明在构造性序数理论中的应用。
We present two seemingly different definitions of constructive ordinal exponentiation, where an ordinal is taken to be a transitive, extensional, and wellfounded order on a set. The first definition is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpiński based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. Our work takes place in the framework of homotopy type theory, and all results are formalized in the proof assistant Agda.