----------------------------------------------------------------------------------------------------
-- Constructive Notions of Ordinals in Homotopy Type Theory
----------------------------------------------------------------------------------------------------

{- Cubical Agda implementation ordinals by Tom de Jong, Nicolai Kraus,
   Fredrik Nordvall-Forsberg, and Chuangjie Xu.

   Source files can be found at

     https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/

   See `README.md` for versions of Agda and the cubical library that these
   files are tested with.
-}

{-# OPTIONS --cubical #-}

module Everything where

{- An axiomatic approach to ordinals -}
import Abstract.ZerSucLim
import Abstract.Arithmetic

import General-Properties
import InfinitelyDescendingSequences

{- Cantor Normal Forms as subsets of unlabled binary trees -}
import CantorNormalForm.Everything

{- Brouwer Trees as a Quotient Inductive-Inductive Type -}
import BrouwerTree.Everything

{- Extensional Wellfounded Orders -}
import ExtensionalWellfoundedOrder.Everything

{- Interpretation between the Notions -}
import Interpretations.CnfToBrw
import Interpretations.BrwToOrd

import Interpretations.CnfToBrw.Properties

{- Comparisions of efficiency -}
import Comparision.Hardy

{- Marked Extensional Wellfounded orders -}
import MEWO.Everything