----------------------------------------------------------------------
--            A Certified Library of Ordinal Arithmetic
--
--    Nicolai Kraus, Fredrik Nordvall-Forsberg, and Chuangjie Xu
----------------------------------------------------------------------

-- Source files can be found at
--
--   https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/
--
-- and
--
--   https://github.com/cj-xu/OrdinalNotations
--
-- All files are tested with
-- • Agda version 2.6.2 and
-- • Cubical Agda library (commit: 4e9e4f7177c3c625db3fb3249e31fa81035c2d69).

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


-- We define a notation system representing ordinals below ε₀
-- simultaneously with an order relation on it.
import CantorNormalForm.Base

-- The order is wellfounded and thus the notation system allows the
-- principle of transfinite induction.
import CantorNormalForm.Wellfoundedness

-- Every term can be classified as a zero, a successor or a limit.
import CantorNormalForm.Classifiability

-- We construct the ordinary arithmetic operations:
import CantorNormalForm.Addition
import CantorNormalForm.Subtraction
import CantorNormalForm.Multiplication
import CantorNormalForm.Division
import CantorNormalForm.Exponentiation
-- and verified their correctness by showing that they satisfy the
-- equations/rules in their set-theoretic definitions.
import CantorNormalForm.Arithmetic

-- We obtain the commutative Hessenberg arithmetic operations
import CantorNormalForm.HessenbergArithmetic
-- by transporting those on finite hereditary multisets
import FiniteHereditaryMultiset.Everything
-- because finite hereditary multisets are an equivalent system.
import Interpretations.CnfEqFhm