Ordinal exponentiation in homotopy type theory

Tools

de Jong, Tom and Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie; (2025) Ordinal exponentiation in homotopy type theory. In: 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, SGP. ISBN 9798331579005 (https://doi.org/10.1109/LICS65433.2025.00027)

[thumbnail of de-Jong-etal-ACM-IEEE-LICS-2025-Ordinal-exponentiation-in-homotopy-type]
Preview
 Text. Filename: de-Jong-etal-ACM-IEEE-LICS-2025-Ordinal-exponentiation-in-homotopy-type.pdf
Accepted Author Manuscript
License: Creative Commons Attribution 4.0 logo
Download (1MB)| Preview

Abstract

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.

ORCID iDs

de Jong, Tom, Kraus, Nicolai, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Xu, Chuangjie;
CORE (COnnecting REpositories)