Ordinal notations via simultaneous definitions
We define an ordinal notation system simultaneously with its ordering. Our simultaneous definitions generate only the ordinal terms in Cantor normal form which are in one-to-one correspondence with the ordinals below ε₀. We implement the ordinal notation system as inductive-inductive-recursive definitions in Agda. We also prove the transfinite induction principle for our ordinal notations.
An html rendering of the Agda code is available at Chuangjie Xu's GitHub web page.
- Agda version 126.96.36.199
- Agda's standard library Version 1.0.1