-------------------------------------------------------------
- Three equivalent ordinal notation systems in Cubical Agda -
-------------------------------------------------------------
Fredrik Nordvall Forsberg and Chuangjie Xu
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.
The source files are available at
https://github.com/cj-xu/OrdinalNotations
All the files are tested with
• Agda development version 2.6.1
(commit: 4af7b92663d2eb1dd94383b140eb7acfeb1b1eb0)
• Cubical Agda library
(commit: d7e345d3bcaefbc066d057487fca9677de7e29c7)
\begin{code}
{-# OPTIONS --cubical --safe #-}
module index where
import Preliminaries
import SigmaOrd
import MutualOrd
import MutualOrdWithoutNestednessAndRecursion
import HITOrd
import Equivalences
import Arithmetic
import TransfiniteInduction
\end{code}