Martin Escardo

\begin{code}

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

module Ordinals.index where

import Ordinals.Arithmetic
import Ordinals.AdditionProperties
import Ordinals.Brouwer
import Ordinals.BuraliForti                   -- by [1]
import Ordinals.Closure
import Ordinals.Codes
import Ordinals.ConvergentSequence
import Ordinals.CumulativeHierarchy           -- by [2]
import Ordinals.CumulativeHierarchy-Addendum  -- by [2]
import Ordinals.Equivalence
import Ordinals.Indecomposable
import Ordinals.InfProperty
import Ordinals.Injectivity
import Ordinals.LexicographicCompactness
import Ordinals.LexicographicOrder
import Ordinals.Limit
import Ordinals.Maps
import Ordinals.MultiplicationProperties      -- by [2]
import Ordinals.NotationInterpretation
import Ordinals.NotationInterpretation0
import Ordinals.NotationInterpretation1
import Ordinals.NotationInterpretation2
import Ordinals.Notions
import Ordinals.OrdinalOfOrdinals
import Ordinals.OrdinalOfOrdinalsSuprema     -- by [3]
import Ordinals.OrdinalOfTruthValues
import Ordinals.ShulmanTaboo
import Ordinals.SupSum
import Ordinals.Taboos                       -- by [3]
import Ordinals.ToppedArithmetic
import Ordinals.ToppedType
import Ordinals.TrichotomousArithmetic
import Ordinals.TrichotomousType
import Ordinals.Type
import Ordinals.Underlying
import Ordinals.WellOrderArithmetic
import Ordinals.WellOrderTransport
import Ordinals.WellOrderingPrinciple
import Ordinals.WellOrderingTaboo            -- by [4]

\end{code}

[1] Bezem, Coquand, Dybjer and Escardo.
[2] de Jong, Kraus, Nordvall Forsberg, and Xu.
[3] Tom de Jong
[4] Tom de Jong (after Andrew Swan)