We present three ordinal notation systems representing ordinals below ε₀ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. As case studies, we show how basic 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.
An html rendering of the cubical Agda code is available at Chuangjie Xu's GitHub web page.
- Agda development version 2.6.2 (commit: 292237b2da99a57cb2bef78ab38d5d45f9fb316c)
- Cubical Agda library (commit: 233263c7e13bc987382f92c47922820fdcffdb81)