Three Equivalent Ordinal Notation Systems in Cubical Agda
summary
Three concrete ordinal notations for ordinals below ε0 are implemented in Cubical Agda: a subset-of-binary-trees giving canonical Cantor normal forms, a mutual inductive–recursive definition that builds every term with a proof of normal form so the order is decidable, and a higher-inductive-type (quotient) version that forces commutative plus. Equivalences between all three are proved (involving insertion-sort style reordering of exponents) and transported by univalence so operations compute definitionally where expected; choice of representation depends on whether decidability, easy proofs, or quotiented algebra is needed.
AI-written summary · about
chapters (8)
- 0:00Ordinal notation systems
- 2:50Faithful ordinal representations
- 6:03Subsets approach
- 9:36Mutual definitions in Agda
- 12:27Higher inductive types in Cubical Agda
- 15:17Equivalence of systems
- 17:04Conclusion and future work
- 17:37Q&A
related talks
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
30mNormalisation for First-Class Universe Levels
27mCanonicity for Indexed Inductive-Recursive Types
01h 08mType Arithmetic and the Yoneda Lemma
26mObservational Equality: Now for Good
24mAn Order-Theoretic Analysis of Universe Polymorphism
59mUnification Modulo Equational Theories in Languages with Binding Operators
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective