```----------------------------------------------------------------------------------------------------
-- 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 _<_ _≤_

is-add : (A → A → A) → Type _
(∀ 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 = Σ[ f ∈ (A → A → A) ] 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
where

_+_ : A → A → A

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

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⟩ _ _)
```