Three Equivalent Ordinal Notation Systems in Cubical Agda

Forsberg, Fredrik Nordvall; Xu, Chuangjie und Ghani, Neil (2020): Three Equivalent Ordinal Notation Systems in Cubical Agda. In: CPP '20: Proceedings of the 9Th Acm Sigplan International Conference on Certified Programs and Proofs: S. 172-185

Abstract

We present three ordinal notation systems representing ordinals below epsilon(0) in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Mathematik
• Themengebiete: 500 Naturwissenschaften und Mathematik > 510 Mathematik
• Sprache: Englisch