Martin Escardo, 2012, 2018, 2022.

See the various imported files for discussion, starting from
OrdinalNotationInterpretation1.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Ordinals.NotationInterpretation where

import Ordinals.NotationInterpretation0 -- Brouwer codes (2022)
import Ordinals.NotationInterpretation1 -- Variation of Brouwer codes (2018)
import Ordinals.NotationInterpretation2 -- Inductive-recursive extension of 1 (2022)

\end{code}