Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
6 November 2024
Refactored between November 2024 and January 2025.

We define types expressing what ordinal exponentiation should be for zero,
successor and supremum exponents, and we record a few properties that follow
immediately follow from those specifications.

\begin{code}

{-# OPTIONS --safe --without-K --exact-split #-}

open import UF.PropTrunc
open import UF.Size
open import UF.Univalence

module Ordinals.Exponentiation.Specification
       (ua : Univalence)
       (pt : propositional-truncations-exist)
       (sr : Set-Replacement pt)
       where

open import MLTT.Spartan
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.UniverseEmbedding

private
 fe : FunExt
 fe = Univalence-gives-FunExt ua

 fe' : Fun-Ext
 fe' = Univalence-gives-Fun-Ext ua

open import Ordinals.AdditionProperties ua
open import Ordinals.Arithmetic fe
open import Ordinals.Maps
open import Ordinals.MultiplicationProperties ua
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.OrdinalOfOrdinalsSuprema ua
open import Ordinals.Type
open import Ordinals.Underlying

open PropositionalTruncation pt
open suprema pt sr

\end{code}

In what follows F should be thought of as implementing ordinal exponentiation
with base Ξ±, i.e. F Ξ² produces the ordinal Ξ±^Ξ².

The three requirements below, together with πŸ˜β‚’^Ξ² ＝ πŸ˜β‚€ for Ξ² β‰  πŸ˜β‚€, classically
*define* ordinal exponentiation.

\begin{code}

module _
        {𝓀 π“₯ : Universe}
        (Ξ± : Ordinal 𝓀)
        (F : Ordinal π“₯ β†’ Ordinal (𝓀 βŠ” π“₯))
       where

 exp-specification-zero : (𝓀 βŠ” π“₯) ⁺ Μ‡
 exp-specification-zero = F (πŸ˜β‚’ {π“₯}) ＝ πŸ™β‚’

 exp-specification-succ : (𝓀 βŠ” π“₯) ⁺ Μ‡
 exp-specification-succ = (Ξ² : Ordinal π“₯) β†’ F (Ξ² +β‚’ πŸ™β‚’) ＝ (F Ξ² Γ—β‚’ Ξ±)

 exp-specification-sup-generalized : (𝓀 βŠ” π“₯) ⁺ Μ‡
 exp-specification-sup-generalized =
  Ξ± β‰  πŸ˜β‚’ β†’ {I : π“₯ Μ‡  } β†’ βˆ₯ I βˆ₯ β†’ (Ξ² : I β†’ Ordinal π“₯)
         β†’ F (sup Ξ²) ＝ sup (Ξ» (i : Lift 𝓀 I) β†’ F (Ξ² (lower i)))

module _
        (Ξ± : Ordinal 𝓀)
        (F : Ordinal 𝓀 β†’ Ordinal 𝓀)
       where

 exp-specification-sup : 𝓀 ⁺ Μ‡
 exp-specification-sup =
  Ξ± β‰  πŸ˜β‚’ β†’ {I : 𝓀 Μ‡  } β†’ βˆ₯ I βˆ₯ β†’ (Ξ² : I β†’ Ordinal 𝓀)
         β†’ F (sup Ξ²) ＝ sup (F ∘ Ξ²)

 exp-specification-sup-from-generalized : exp-specification-sup-generalized Ξ± F
                                        β†’ exp-specification-sup
 exp-specification-sup-from-generalized Οƒ l {I} I-inh Ξ² = Οƒ l I-inh Ξ² βˆ™ e
  where
   e : sup (F ∘ β ∘ lower) ＝ sup (F ∘ β)
   e = ⊴-antisym _ _
        (sup-composition-⊴ lower (F ∘ β))
        (sup-composition-⊴ (lift 𝓀) (F ∘ Ξ² ∘ lower))

\end{code}

Added 29 January 2025 by Tom de Jong.
Minor changes 15 May 2025 by Fredrik Nordvall Forsberg
\begin{code}

 exp-specification-sup-strong : 𝓀 ⁺ Μ‡
 exp-specification-sup-strong =
  (I : 𝓀 Μ‡  ) β†’ (Ξ² : I β†’ Ordinal 𝓀)
             β†’ F (sup Ξ²) ＝ sup (cases {X = πŸ™{𝓀}} (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ²))

 exp-specification-sup-strong-implies-monotonicity
  : exp-specification-sup-strong
  β†’ is-monotone (OO 𝓀) (OO 𝓀) F
 exp-specification-sup-strong-implies-monotonicity Οƒ Ξ² Ξ³ l =
  transport (F Ξ² β‰Ό_) (ap F (e ⁻¹)) k
   where
    Ξ” : πŸ™{𝓀} + πŸ™{𝓀} β†’ Ordinal 𝓀
    Ξ” = cases (Ξ» _ β†’ Ξ²) (Ξ» _ β†’ Ξ³)
    e : Ξ³ ＝ sup Ξ”
    e = ⊴-antisym Ξ³ (sup Ξ”)
         (sup-is-upper-bound Ξ” (inr ⋆))
         (sup-is-lower-bound-of-upper-bounds Ξ” Ξ³
           (dep-cases (Ξ» _ β†’ β‰Ό-gives-⊴ Ξ² Ξ³ l) (Ξ» _ β†’ ⊴-refl Ξ³)))
    k : F Ξ² β‰Ό F (sup Ξ”)
    k = transport⁻¹ (F Ξ² β‰Ό_)
                    (Οƒ (πŸ™ + πŸ™) Ξ”)
                    (⊴-gives-β‰Ό (F Ξ²)
                      (sup (cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ”)))
                      (sup-is-upper-bound _ (inr (inl ⋆))))

 exp-specification-zero-from-strong-sup-specification
  : exp-specification-sup-strong
  β†’ exp-specification-zero Ξ± F
 exp-specification-zero-from-strong-sup-specification Οƒ =
  F πŸ˜β‚’      ＝⟨ ap F I ⟩
  F (sup Ξ΅) ＝⟨ Οƒ 𝟘 Ξ΅ ⟩
  sup Ρ'    ＝⟨ II ⟩
  πŸ™β‚’        ∎
   where
    Ξ΅ : 𝟘 β†’ Ordinal 𝓀
    Ρ = 𝟘-elim
    Ξ΅' : πŸ™ + 𝟘 β†’ Ordinal 𝓀
    Ξ΅' = cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ΅)
    I : πŸ˜β‚’ ＝ sup Ξ΅
    I = ⊴-antisym πŸ˜β‚’ (sup Ξ΅)
         (πŸ˜β‚’-least-⊴ (sup Ξ΅))
         (sup-is-lower-bound-of-upper-bounds Ξ΅ πŸ˜β‚’ 𝟘-induction)
    II : sup Ξ΅' ＝ πŸ™β‚’
    II = ⊴-antisym (sup Ξ΅') πŸ™β‚’
          (sup-is-lower-bound-of-upper-bounds Ξ΅' πŸ™β‚’
            (dep-cases (Ξ» _ β†’ ⊴-refl πŸ™β‚’) 𝟘-induction))
          (sup-is-upper-bound Ξ΅' (inl ⋆))

 exp-specification-sup-from-strong : exp-specification-sup-strong
                                   β†’ exp-specification-sup
 exp-specification-sup-from-strong specβ‚› Ξ±-nonzero {I} I-inh Ξ² =
  F (sup Ξ²)                      ＝⟨ specβ‚› I Ξ² ⟩
  sup (cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ²)) ＝⟨ e ⟩
  sup (F ∘ β)                    ∎
   where
    specβ‚€ : exp-specification-zero Ξ± F
    specβ‚€ = exp-specification-zero-from-strong-sup-specification specβ‚›
    F-monotone : is-monotone (OO 𝓀) (OO 𝓀) F
    F-monotone = exp-specification-sup-strong-implies-monotonicity specβ‚›
    e = ⊴-antisym _ _
         (sup-is-lower-bound-of-upper-bounds
           (cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ²))
           (sup (F ∘ β)) ub)
         (sup-composition-⊴ inr (cases (Ξ» _ β†’ πŸ™β‚’) (Ξ» x β†’ F (Ξ² x))))
     where
      ub : (x : πŸ™ + I) β†’ cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ²) x ⊴ sup (F ∘ Ξ²)
      ub (inr i) = sup-is-upper-bound (F ∘ β) i
      ub (inl ⋆) = βˆ₯βˆ₯-rec (⊴-is-prop-valued πŸ™β‚’ (sup (F ∘ Ξ²))) ub' I-inh
       where
        ub' : I β†’ πŸ™β‚’ ⊴ sup (F ∘ Ξ²)
        ub' i = ⊴-trans πŸ™β‚’ (F (Ξ² i)) (sup (F ∘ Ξ²))
                 (β‰Ό-gives-⊴ πŸ™β‚’ (F (Ξ² i))
                   (transport (_β‰Ό F (Ξ² i))
                              specβ‚€
                              (F-monotone πŸ˜β‚’ (Ξ² i) (πŸ˜β‚’-least (Ξ² i)))))
                 (sup-is-upper-bound (F ∘ β) i)

 exp-specification-sup-strong-if-EM : EM 𝓀
                                    β†’ Ξ± β‰  πŸ˜β‚’
                                    β†’ exp-specification-zero Ξ± F
                                    β†’ exp-specification-sup
                                    β†’ exp-specification-sup-strong
 exp-specification-sup-strong-if-EM em Ξ±-nonzero specβ‚€ specβ‚› I Ξ² =
  ΞΊ (em βˆ₯ I βˆ₯ βˆ₯βˆ₯-is-prop)
  where
    G : πŸ™ + I β†’ Ordinal 𝓀
    G = cases (Ξ» _ β†’ πŸ™β‚’) (F ∘ Ξ²)
    ΞΊ : is-decidable βˆ₯ I βˆ₯ β†’ F (sup Ξ²) ＝ sup G
    ΞΊ (inl I-inh) = βˆ₯βˆ₯-rec (underlying-type-is-set fe (OO 𝓀)) h I-inh
     where
      h : I β†’ F (sup Ξ²) ＝ sup G
      h i = F (sup Ξ²) ＝⟨ specβ‚› Ξ±-nonzero I-inh Ξ² ⟩
            sup (F ∘ Ξ²) ＝⟨ ⊴-antisym (sup (F ∘ Ξ²)) (sup G) h₁ hβ‚‚ ⟩
            sup G ∎
       where
        h₁ : sup (F ∘ Ξ²) ⊴ sup G
        h₁ = sup-composition-⊴ inr G
        hβ‚‚ : sup G ⊴ sup (F ∘ Ξ²)
        hβ‚‚ = sup-is-lower-bound-of-upper-bounds G (sup (F ∘ Ξ²)) h₃
         where
          h₃ : (x : πŸ™ + I) β†’ G x ⊴ sup (F ∘ Ξ²)
          h₃ (inr i) = sup-is-upper-bound (F ∘ Ξ²) i
          h₃ (inl ⋆) =
           ⊴-trans πŸ™β‚’ (F (Ξ² i)) (sup (F ∘ Ξ²))
            (β‰Ό-gives-⊴ πŸ™β‚’ (F (Ξ² i))
              (transport (_β‰Ό F (Ξ² i))
                         specβ‚€
                         (is-monotone-if-continuous F
                           (specβ‚› Ξ±-nonzero)
                           πŸ˜β‚’
                           (Ξ² i)
                           (πŸ˜β‚’-least (Ξ² i)))))
            (sup-is-upper-bound (F ∘ β) i)
    ΞΊ (inr I-empty) =
     F (sup Ξ²) ＝⟨ ap F e₁ ⟩
     F πŸ˜β‚’      ＝⟨ specβ‚€ ⟩
     πŸ™β‚’        ＝⟨ eβ‚‚ ⁻¹ ⟩
     sup G     ∎
      where
       e₁ : sup Ξ² ＝ πŸ˜β‚’
       e₁ = ⊴-antisym (sup Ξ²) πŸ˜β‚’
             (sup-is-lower-bound-of-upper-bounds Ξ² πŸ˜β‚’
               (Ξ» i β†’ 𝟘-elim (I-empty ∣ i ∣)))
             (πŸ˜β‚’-least-⊴ (sup Ξ²))
       eβ‚‚ : sup G ＝ πŸ™β‚’
       eβ‚‚ = ⊴-antisym (sup G) πŸ™β‚’
             (sup-is-lower-bound-of-upper-bounds G πŸ™β‚’
               (dep-cases (Ξ» _ β†’ ⊴-refl πŸ™β‚’) (Ξ» i β†’ 𝟘-elim (I-empty ∣ i ∣))))
             (sup-is-upper-bound G (inl ⋆))

\end{code}

The appealing thing about the strong supremum specification is that, together
with the successor specification, it uniquely specifies exponentiation with a
nonzero base.

\begin{code}

exp-strong-specification-uniquely-specifies-exp'
 : (Ξ± : Ordinal 𝓀)
 β†’ (F G : Ordinal 𝓀 β†’ Ordinal 𝓀)
 β†’ exp-specification-sup-strong Ξ± F
 β†’ exp-specification-succ Ξ± F
 β†’ exp-specification-sup-strong Ξ± G
 β†’ exp-specification-succ Ξ± G
 β†’ F ∼ G
exp-strong-specification-uniquely-specifies-exp' {𝓀} Ξ± F G F-eq₁ F-eqβ‚‚ G-eq₁ G-eqβ‚‚ =
 transfinite-induction-on-OO _ e
  where
   e : (Ξ² : Ordinal 𝓀)
     β†’ ((b : ⟨ Ξ² ⟩) β†’ F (Ξ² ↓ b) ＝ G (Ξ² ↓ b))
     β†’ F Ξ² ＝ G Ξ²
   e Ξ² IH =
     F β                                              ＝⟨ I   ⟩
     F (sup Ξ» b β†’ (Ξ² ↓ b) +β‚’ πŸ™β‚’)                      ＝⟨ II  ⟩
     sup (cases (Ξ» _ β†’ πŸ™β‚’) (Ξ» b β†’ F ((Ξ² ↓ b) +β‚’ πŸ™β‚’))) ＝⟨ III ⟩
     sup (cases (Ξ» _ β†’ πŸ™β‚’) (Ξ» b β†’ F (Ξ² ↓ b) Γ—β‚’ Ξ±))    ＝⟨ IV  ⟩
     sup (cases (Ξ» _ β†’ πŸ™β‚’) (Ξ» b β†’ G (Ξ² ↓ b) Γ—β‚’ Ξ±))    ＝⟨ V   ⟩
     sup (cases (Ξ» _ β†’ πŸ™β‚’) (Ξ» b β†’ G ((Ξ² ↓ b) +β‚’ πŸ™β‚’))) ＝⟨ VI  ⟩
     G (sup (Ξ» b β†’ (Ξ² ↓ b) +β‚’ πŸ™β‚’))                    ＝⟨ VII ⟩
     G β                                              ∎
      where
       I   = ap F (supremum-of-successors-of-initial-segments pt sr Ξ²)
       II  = F-eq₁ ⟨ Ξ² ⟩ (Ξ» b β†’ (Ξ² ↓ b) +β‚’ πŸ™β‚’)
       III = ap (Ξ» - β†’ sup (cases (Ξ» (_ : πŸ™{𝓀}) β†’ πŸ™β‚’) -))
                (dfunext fe' (Ξ» b β†’ F-eqβ‚‚ (Ξ² ↓ b)))
       IV  = ap (Ξ» - β†’ sup (cases (Ξ» (_ : πŸ™{𝓀}) β†’ πŸ™β‚’) -))
                (dfunext fe' (Ξ» b β†’ ap (_Γ—β‚’ Ξ±) (IH b)))
       V   = ap (Ξ» - β†’ sup (cases (Ξ» (_ : πŸ™{𝓀}) β†’ πŸ™β‚’) -))
                (dfunext fe' (Ξ» b β†’ (G-eqβ‚‚ (Ξ² ↓ b)) ⁻¹))
       VI  = (G-eq₁ ⟨ Ξ² ⟩ (Ξ» b β†’ (Ξ² ↓ b) +β‚’ πŸ™β‚’)) ⁻¹
       VII = ap G ((supremum-of-successors-of-initial-segments pt sr β) ⁻¹)

exp-strong-specification-uniquely-specifies-exp
 : (Ξ± : Ordinal 𝓀)
 β†’ Ξ± β‰  πŸ˜β‚’
 β†’ is-prop (Ξ£ F κž‰ (Ordinal 𝓀 β†’ Ordinal 𝓀) , exp-specification-sup-strong Ξ± F
                                          Γ— exp-specification-succ Ξ± F)
exp-strong-specification-uniquely-specifies-exp {𝓀} Ξ± Ξ±-nonzero =
 (Ξ» (F , F-eq₁ , F-eqβ‚‚) (G , G-eq₁ , G-eqβ‚‚)
   β†’ to-subtype-＝
      (Ξ» H β†’ Γ—-is-prop
              (Ξ β‚‚-is-prop fe' (Ξ» _ _ β†’ underlying-type-is-set fe (OO 𝓀)))
              (Ξ -is-prop fe' (Ξ» _ β†’ underlying-type-is-set fe (OO 𝓀))))
              (dfunext fe'
                (exp-strong-specification-uniquely-specifies-exp' Ξ±
                  F G F-eq₁ F-eqβ‚‚ G-eq₁ G-eqβ‚‚)))

\end{code}

The following special cases follow directly from the specification.

\begin{code}

module _
        (Ξ± : Ordinal 𝓀)
        (exp-Ξ± : Ordinal 𝓀 β†’ Ordinal 𝓀)
        (exp-zero : exp-specification-zero Ξ± exp-Ξ±)
        (exp-succ : exp-specification-succ Ξ± exp-Ξ±)
 where

 πŸ™β‚’-neutral-exp : exp-Ξ± πŸ™β‚’ ＝ Ξ±
 πŸ™β‚’-neutral-exp =
  exp-Ξ± πŸ™β‚’             ＝⟨ ap (exp-Ξ±) (πŸ˜β‚’-left-neutral πŸ™β‚’ ⁻¹)  ⟩
  exp-Ξ± (πŸ˜β‚’ {𝓀} +β‚’ πŸ™β‚’) ＝⟨ exp-succ πŸ˜β‚’ ⟩
  exp-Ξ± (πŸ˜β‚’) Γ—β‚’ Ξ±      ＝⟨ ap (_Γ—β‚’ Ξ±) exp-zero ⟩
  πŸ™β‚’ Γ—β‚’ Ξ±              ＝⟨ πŸ™β‚’-left-neutral-Γ—β‚’ Ξ± ⟩
  α                    ∎

 exp-πŸšβ‚’-is-Γ—β‚’ : exp-Ξ± πŸšβ‚’ ＝ Ξ± Γ—β‚’ Ξ±
 exp-πŸšβ‚’-is-Γ—β‚’ =
  exp-Ξ± (πŸ™β‚’ +β‚’ πŸ™β‚’) ＝⟨ exp-succ πŸ™β‚’ ⟩
  exp-Ξ± πŸ™β‚’ Γ—β‚’ Ξ±    ＝⟨ ap (_Γ—β‚’ Ξ±) πŸ™β‚’-neutral-exp ⟩
  Ξ± Γ—β‚’ Ξ±           ∎

\end{code}

The specification for suprema implies monotonicity.

\begin{code}

exp-is-monotone-in-exponent : (Ξ± : Ordinal 𝓀)
                              (exp-Ξ± : Ordinal π“₯ β†’ Ordinal (𝓀 βŠ” π“₯))
                            β†’ (Ξ± β‰  πŸ˜β‚’)
                            β†’ exp-specification-sup-generalized Ξ± exp-Ξ±
                            β†’ is-monotone (OO π“₯) (OO (𝓀 βŠ” π“₯)) exp-Ξ±
exp-is-monotone-in-exponent Ξ± exp-Ξ± Ξ½ exp-sup =
 is-monotone-if-continuous-generalized exp-Ξ± (exp-sup Ξ½)

\end{code}