Three Equivalent Ordinal Notation Systems in Cubical Agda

TL;DR

This paper introduces three equivalent ordinal notation systems in cubical Agda, utilizing recent type-theoretical innovations to represent and manipulate ordinals below _0, with formal proofs of their equivalence and implementations.

Contribution

It presents three new ordinal notation systems in type theory, demonstrating their equivalence and enabling transfer of results via univalence, implemented in cubical Agda.

Findings

All three systems are proven equivalent.

Ordinal arithmetic and transfinite induction are developed for these systems.

Implementations are provided in cubical Agda.

Abstract

We present three ordinal notation systems representing ordinals below $\varepsilon_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.