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

{- Cubical Agda implementation of the paper

     Connecting Constructive Notions of Ordinals in Homotopy Type Theory

         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

{- 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