--------------------------------------------------
          Ordinal notations via simultaneous definitions
        --------------------------------------------------

            Fredrik Nordvall Forsberg and Chuangjie Xu


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.

The source files are available at

    https://github.com/cj-xu/OrdinalNotations

All the files are tested in the safe mode of Agda version 2.6.0.1 with
Agda's standard library Version 1.0.1.

\begin{code}

{-# OPTIONS --safe #-}

\end{code}

■ An inductive-inductive-recursive definition of ordinal notations

Our ordinal notations are nested weakly decreasing lists.  When
inserting a new element x in front of an already constructed list xs,
we need to ensure that x is greater than or equal to the head of xs.
Therefore, we simultaneously define an inductive type 𝒪 of ordinal
notations, an inductive family of types a < b indexed by a,b : 𝒪, and
a head function fst: 𝒪 → 𝒪.

\begin{code}

import OrdinalNotations

\end{code}

■ Ordinal arithmetic

We define ordinal arithmetic operations for our ordinal notations
including addition, subtraction, multiplication and exponentiation.

\begin{code}

import OrdinalArithmetic

\end{code}

■ Transfinite induction

We prove that our simultaneous definition 𝒪 of ordinal notations is
well-founded and hence have the transfinite induction principle for 𝒪.
Using this, we prove a computational version of the statement

  there is no infinite descending sequence of ordinals below ε₀.

\begin{code}

import TransfiniteInduction

\end{code}

■ An equivalent inductive-inductive definition of ordinal notations

The head function fst : 𝒪 → 𝒪 is only used strictly positively in 𝒪
and <, which means that its graph can be defined inductive-inductively
and in turn used instead of the recursively defined fst.  This reduces
the above inductive-inductive-recursive construction to an
inductive-inductive one.

\begin{code}

import OrdinalNotationsWithoutRecursion

\end{code}