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 Bezem, Coquand, Dybjer and Escardo.
import Ordinals.Closure
import Ordinals.Codes
import Ordinals.ConvergentSequence
import Ordinals.CumulativeHierarchy           -- by de Jong, Kraus, Nordvall Forsberg, and Xu.
import Ordinals.CumulativeHierarchy-Addendum  -- by de Jong, Kraus, Nordvall Forsberg, and Xu.
import Ordinals.Equivalence
import Ordinals.Indecomposable
import Ordinals.Injectivity
import Ordinals.LexicographicOrder
import Ordinals.Maps
import Ordinals.MultiplicationProperties      -- by de Jong, Kraus, Nordvall Forsberg, and Xu.
import Ordinals.NotationInterpretation
import Ordinals.NotationInterpretation0
import Ordinals.NotationInterpretation1
import Ordinals.NotationInterpretation2
import Ordinals.Notions
import Ordinals.OrdinalOfOrdinals
import Ordinals.OrdinalOfOrdinalsSuprema     -- by Tom de Jong
import Ordinals.OrdinalOfTruthValues
import Ordinals.ShulmanTaboo
import Ordinals.SupSum
import Ordinals.Taboos                       -- by Tom de Jong
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 Tom de Jong (after Andrew Swan)

\end{code}