Martin Escardo, with additions by others, indicated below.

\begin{code}

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

module Ordinals.index where

import Ordinals.AdditionProperties
import Ordinals.Arithmetic
import Ordinals.ArithmeticReflection          -- by [2]
import Ordinals.BoundedOperations             -- by [2]
import Ordinals.BrouwerCodes
import Ordinals.BrouwerCodesInterpretations
import Ordinals.BrouwerCodesVariationInterpretations
import Ordinals.BuraliForti                   -- by [1]
import Ordinals.ChurchEncoding
import Ordinals.Closure
import Ordinals.CompactnessOfSuprema
import Ordinals.ConvergentSequence
import Ordinals.CumulativeHierarchy           -- by [2]
import Ordinals.CumulativeHierarchy-Addendum  -- by [2]
import Ordinals.Equivalence
import Ordinals.Exponentiation.index          -- by [2]
import Ordinals.FailureOfTotalSeparatedness
import Ordinals.FailureOfTrichotomy
import Ordinals.Fin                           -- by [5] with additions by [2]
import Ordinals.IdentifyingEquivalentOrdinals -- by [3]
import Ordinals.Indecomposable
import Ordinals.InductiveRecursiveCodesInterpretations
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.Notions
import Ordinals.Omega                        -- by [2]
import Ordinals.OrdinalOfOrdinals
import Ordinals.OrdinalOfOrdinalsSuprema     -- by [3]
import Ordinals.OrdinalOfTruthValues
import Ordinals.Propositions
import Ordinals.ShulmanTaboo
import Ordinals.SupSum
import Ordinals.Taboos                       -- by [3]
import Ordinals.ToppedArithmetic
import Ordinals.ToppedType
import Ordinals.TotallySeparated
import Ordinals.TrichotomousArithmetic
import Ordinals.TrichotomousType
import Ordinals.Two
import Ordinals.Type
import Ordinals.Underlying
import Ordinals.WellOrderArithmetic
import Ordinals.WellOrderExtension
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)
[5] Alice Laroche