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



   All the files are tested with

   • Agda development version 2.6.2
     (commit: 2479f0a7122a41ac15f5699dc87ed41ed72cbd0e)

   • Cubical Agda library
     (commit: 745b29ac154d07e05fd6d1709d0983b863541afc)
-}

{-# OPTIONS --cubical #-}

module index 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