----------------------------------------------------------------------------------------------------
-- Axioms for ordinals arithmetic
----------------------------------------------------------------------------------------------------

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary

module Abstract.Arithmetic
  {i j k}
  {A : Type i}
  (_<_ : A  A  Type j)
  (_≤_ : A  A  Type k)
  where

open import Abstract.ZerSucLim _<_ _≤_


{- Addition -}

is-add : (A  A  A)  Type _
is-add _+_ =
  (∀ a c  is-zero a  c + a  c) ×
  (∀ a b c d  a is-suc-of b  d is-suc-of (c + b)  c + a  d) ×
  (∀ a b c f f↑  a is-lim-of (f , f↑)  b is-sup-of  i  c + f i)  c + a  b)

has-add : Type _
has-add = Σ[ f  (A  A  A) ] is-add f

has-unique-add : Type _
has-unique-add = isContr has-add

isProp⟨is-add⟩ : isSet A   f  isProp (is-add f)
isProp⟨is-add⟩ isSet⟨A⟩ _ = isProp×2 (isPropΠ3 λ _ _ _  isSet⟨A⟩ _ _)
                                     (isPropΠ2 λ _ _  isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)
                                     (isPropΠ3 λ _ _ _  isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)

{- Multiplication -}

module Multiplication
  (add : has-add)
  where

  _+_ : A  A  A
  _+_ = fst add

  is-mul : (A  A  A)  Type _
  is-mul _·_ =
    (∀ a c  is-zero a  c · a  a) ×
    (∀ a b c  a is-suc-of b  c · a  (c · b) + c) ×
    (∀ a b c f f↑  a is-lim-of (f , f↑)  b is-sup-of  i  c · f i)  c · a  b)

  has-mul : Type _
  has-mul = Σ[ f  (A  A  A) ] is-mul f

  has-unique-mul : Type _
  has-unique-mul = isContr has-mul

  isProp⟨is-mul⟩ : isSet A   f  isProp (is-mul f)
  isProp⟨is-mul⟩ isSet⟨A⟩ _ = isProp×2 (isPropΠ3 λ _ _ _  isSet⟨A⟩ _ _)
                                       (isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)
                                       (isPropΠ3 λ _ _ _  isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)

{- Exponentiation -}

module Exponentiation
  (add : has-add)
  (mul : Multiplication.has-mul add)
  where

  _·_ : A  A  A
  _·_ = fst mul

  _is-exp-with-base_ : (A  A)  A  Type _
  c^_ is-exp-with-base c =
    (∀ a b    is-zero a  b is-suc-of a  c^ a  b) ×
    (∀ a b    a is-suc-of b  c^ a  (c^ b) · c) ×
    (∀ a b f f↑  a is-lim-of (f , f↑)  ¬ is-zero c  b is-sup-of  i  c^ f i)  c^ a  b) ×
    (∀ a   f f↑  a is-lim-of (f , f↑)    is-zero c                               c^ a  c)

  has-exp-with-base : A  Type _
  has-exp-with-base c = Σ[ f  (A  A) ] f is-exp-with-base c

  has-unique-exp-with-base : A  Type _
  has-unique-exp-with-base c = isContr (has-exp-with-base c)

  has-unique-exp : Type _
  has-unique-exp =  c  has-unique-exp-with-base c

  isProp⟨is-exp⟩ : isSet A   c f  isProp (f is-exp-with-base c)
  isProp⟨is-exp⟩ isSet⟨A⟩ _ _ = isProp×3 (isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)
                                         (isPropΠ3 λ _ _ _  isSet⟨A⟩ _ _)
                                         (isPropΠ3 λ _ _ _  isPropΠ4 λ _ _ _ _  isSet⟨A⟩ _ _)
                                         (isPropΠ3 λ _ _ _  isPropΠ2 λ _ _  isSet⟨A⟩ _ _)