=============================
 =                           =
 =  Example: majorizability  =
 =                           =
 =============================

    Chuangjie Xu, July 2019


References.

□ William A. Howard.  Hereditarily majorizable functionals of finite
  type.  In Metamathematical investigation of intuitionistic
  Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics,
  pages 454–461. Springer, Berlin, 1973.

\begin{code}

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

open import Preliminaries
open import T

module Majorizability where

\end{code}

■ A nucleus for majorants

\begin{code}

κ : (ℕ → ℕ) → ℕ → ℕ
κ = φ
-- κ g  0       = g 0
-- κ g (succ n) = max (κ g n) (g (succ n))

KE : {ρ : Ty} → (ℕ → ⟦ ρ ⟧ʸ) → ℕ → ⟦ ρ ⟧ʸ
KE {ι}     g = κ g
KE {_ ⇾ ρ} g = λ n a → KE (λ x → g x a) n

⟦_⟧ᴶ : {Γ : Cxt} {ρ : Ty} → T Γ ρ → ⟦ Γ ⟧ˣ → ⟦ ρ ⟧ʸ
⟦ Var i ⟧ᴶ γ = γ ₍ i ₎
⟦ Lam t ⟧ᴶ γ = λ a → ⟦ t ⟧ᴶ (γ , a)
⟦ f · a ⟧ᴶ γ = ⟦ f ⟧ᴶ γ (⟦ a ⟧ᴶ γ)
⟦ Zero ⟧ᴶ  _ = zero
⟦ Succ ⟧ᴶ  _ = succ
⟦ Rec ⟧ᴶ   _ = λ a f → KE (rec a f)

infixl  _ᴶ

_ᴶ : {ρ : Ty} → T ε ρ → ⟦ ρ ⟧ʸ
t ᴶ = ⟦ t ⟧ᴶ ⋆

\end{code}

■ Theorem: Every closed term t is majoraized by its J-translation.

\begin{code}

_maj_ : {ρ : Ty} → ⟦ ρ ⟧ʸ → ⟦ ρ ⟧ʸ → Set
_maj_ {ι}     n m = n ≥ m
_maj_ {σ ⇾ τ} f g = {x y : ⟦ σ ⟧ʸ} → x maj y → (f x) maj (g y)

Theorem : {ρ : Ty} (t : T ε ρ) → t ᴶ maj ⟦ t ⟧

\end{code}

■ Proof

\begin{code}

_majˣ_ : {Γ : Cxt} → ⟦ Γ ⟧ˣ → ⟦ Γ ⟧ˣ → Set
_majˣ_ {ε}      ⋆       ⋆      = 𝟙
_majˣ_ {Γ ₊ ρ} (δ , x) (γ , y) = (δ majˣ γ) × (x maj y)

maj[Var] : {Γ : Cxt} {ρ : Ty} {δ : ⟦ Γ ⟧ˣ} {γ : ⟦ Γ ⟧ˣ}
         → δ majˣ γ → (i : ∥ ρ ∈ Γ ∥) → (δ ₍ i ₎) maj (γ ₍ i ₎)
maj[Var] (_ , θ)  zero    = θ
maj[Var] (ζ , _) (succ i) = maj[Var] ζ i

maj[KE] : {ρ : Ty}
        → {f g : ℕ → ⟦ ρ ⟧ʸ} → ((i : ℕ) → (f i) maj (g i))
        → (KE f) maj g
maj[KE] {ι}     ζ χ = ≤trans (ζ _) (φ-spec χ)
maj[KE] {σ ⇾ τ} ζ χ = λ ξ → maj[KE] (λ i → ζ i ξ) χ

Lemma[maj] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ)
           → {δ γ : ⟦ Γ ⟧ˣ} → δ majˣ γ
           → (⟦ t ⟧ᴶ δ) maj (⟦ t ⟧ᵐ γ)
Lemma[maj] (Var i) ζ = maj[Var] ζ i
Lemma[maj] (Lam t) ζ = λ θ → Lemma[maj] t (ζ , θ)
Lemma[maj] (f · a) ζ = Lemma[maj] f ζ (Lemma[maj] a ζ)
Lemma[maj]  Zero   ζ = ≤zero
Lemma[maj]  Succ   ζ = ≤succ
Lemma[maj]  Rec    ζ {x} {y} χ {f} {g} ξ = maj[KE] claim
 where
  claim : (i : ℕ) → rec x f i maj rec y g i
  claim         = χ
  claim (succ i) = ξ ≤refl (claim i)

{-
Theorem : {ρ : Ty} (t : Τ ε ρ) → t ᴶ maj ⟦ t ⟧
-}
Theorem t = Lemma[maj] t {⋆} {⋆} ⋆

\end{code}