----------------------------------------------------------------------------------------------------
-- Cantor Normal Forms
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module CantorNormalForm.Everything where

{- Definition and properties -}
open import CantorNormalForm.Base public

{- Wellfoundedness -}
open import CantorNormalForm.Wellfoundedness public

{- Arithmetic operations and their correctness -}
open import CantorNormalForm.Arithmetic public

{- Classifiability -}
open import CantorNormalForm.Classifiability public

{- Some taboos about Cnf having limits of bounded sequences -}
open import CantorNormalForm.LimitsAndTaboos public