--------------------------------------------------------------------------------
author:         Ayberk Tosun
date-started:   2023-10-07
date-completed: 2023-12-30
dates-updated:  [2024-03-12]
--------------------------------------------------------------------------------

Continuation of the development in `InternalModCont` towards uniform continuity.

\begin{code}

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

open import UF.FunExt
open import UF.Equiv hiding (⌜_⌝)
open import UF.Retracts

module EffectfulForcing.Internal.InternalModUniCont (fe : Fun-Ext) where

open import EffectfulForcing.Internal.Correctness
 using (Rnorm; Rnorm-generic; Rnorm-lemma₀; is-dialogue-for)
open import EffectfulForcing.Internal.External
 using (B⟦_⟧; B⟦_⟧₀; dialogue-tree; eloquence-theorem; ⟪⟫)
open import EffectfulForcing.Internal.Internal
open import EffectfulForcing.Internal.InternalModCont fe
 using (maxᵀ; maxᵀ-correct)
open import EffectfulForcing.Internal.Subst
open import EffectfulForcing.Internal.SystemT
open import EffectfulForcing.MFPSAndVariations.Church
open import EffectfulForcing.MFPSAndVariations.Combinators
open import EffectfulForcing.MFPSAndVariations.Continuity
 using (is-continuous; _＝⟪_⟫_; C-restriction; Cantor; Baire;
        is-uniformly-continuous; _＝⟦_⟧_; BT; embedding-𝟚-ℕ)
open import EffectfulForcing.MFPSAndVariations.ContinuityProperties fe
open import EffectfulForcing.MFPSAndVariations.Dialogue
 using (B; C; D; dialogue-continuity; dialogue; eloquent-functions-are-UC;
        eloquent-functions-are-continuous; eloquent; generic; prune;
        restriction-is-eloquent; dialogue-UC)
open import EffectfulForcing.MFPSAndVariations.SystemT
 using (type; ι; _⇒_;〖_〗)
open import MLTT.List
open import MLTT.Spartan hiding (rec; _^_)
open import Naturals.Order using (max)

\end{code}

First, we define some nicer syntax for inherently typed System T terms.

\begin{code}

_⊢_ : Cxt → type → 𝓤₀  ̇
_⊢_ Γ τ = T Γ τ

infix 4 _⊢_

baire : type
baire = ι ⇒ ι

\end{code}

In module `InternalModCont`, we defined a System T operation that computes
moduli of continuity of maps from Baire space into ℕ. In this module, we develop
the same operation for maps on the Cantor space -- but this time it computes
the modulus of _uniform_ continuity.

To define the Cantor type, it's tempting to augment System T with the type of
Booleans. However, we refrain from doing that here as to avoid repeating all our
proofs on System T. Instead, we adopt the approach of working with the `baire`
type under the implicit assumption that its range is `{0, 1}`. We define all
operations on the `baire` type under this assumption, and prove that the modulus
of uniform continuity operation satisfies its specification.

\section{Preliminaries}

We define the functions `to-numeral` and `to-nat`.

  * The function `to-numeral` gives the System T representation of a natural
    number.
  * The function `to-nat` gives the natural number represented by a System T
    numeral.

\begin{code}

to-numeral : ℕ → 〈〉 ⊢ ι
to-numeral = numeral {〈〉}

to-nat : 〈〉 ⊢ ι → ℕ
to-nat t = ⟦ t ⟧₀

\end{code}

The function `to-nat` is a retraction of `to-numeral`.

\begin{code}

to-nat-cancels-to-numeral : to-nat ∘ to-numeral ∼ id
to-nat-cancels-to-numeral zero     = refl
to-nat-cancels-to-numeral (succ n) = ap succ (to-nat-cancels-to-numeral n)

numeral-is-section : is-section to-numeral
numeral-is-section = to-nat , to-nat-cancels-to-numeral

\end{code}

In module `ContinuityProperties`, we defined the notion of a Boolean point. We
now define the same notion for System T representations of points of the Baire
space.

\begin{code}

is-boolean-pointᵀ : 〈〉 ⊢ baire → 𝓤₀  ̇
is-boolean-pointᵀ α =
 (n : 〈〉 ⊢ ι) → (⟦ α ⟧₀ ⟦ n ⟧₀ ＝ 0) + (⟦ α ⟧₀ ⟦ n ⟧₀ ＝ 1)

\end{code}

If a System T term `t` satisfies `is-boolean-pointᵀ`, then its interpretation
`⟦ t ⟧` obviously satisfies `is-boolean-point`.

\begin{code}

boolean-valuedᵀ-lemma : (t : 〈〉 ⊢ baire)
                      → is-boolean-pointᵀ t
                      → is-boolean-point ⟦ t ⟧₀
boolean-valuedᵀ-lemma t ψ i = cases † ‡ (ψ (numeral i))
 where
  ※ = ap ⟦ t ⟧₀ (to-nat-cancels-to-numeral i ⁻¹)

  † : ⟦ t ⟧₀ ⟦ numeral i ⟧₀ ＝ zero → is-boolean-valued (⟦ t ⟧₀ i)
  † p = inl q
   where
    q : ⟦ t ⟧₀ i ＝ 0
    q = ⟦ t ⟧₀ i ＝⟨ ※ ⟩ ⟦ t ⟧₀ ⟦ numeral i ⟧₀ ＝⟨ p ⟩ 0 ∎

  ‡ : ⟦ t ⟧₀ ⟦ numeral i ⟧₀ ＝ 1 → is-boolean-valued (⟦ t ⟧₀ i)
  ‡ p = inr q
   where
    q : ⟦ t ⟧₀ i ＝ 1
    q = ⟦ t ⟧₀ i ＝⟨ ※ ⟩ ⟦ t ⟧₀ ⟦ numeral i ⟧₀ ＝⟨ p ⟩ 1 ∎

\end{code}

Following the conventions of the `InternalModCont` module, we define three
versions of the same operation.

  1. `max-boolean-question`, that works on the external inductive type encoding
     of dialogue trees in Agda,
  2. `max-boolean-question⋆`, that works on the external Church encoding of
     dialogue trees in Agda, and
  3. `max-boolean-questionᵀ`, that is a System T function working on the Church
     encoding of dialogue trees in System T.

\begin{code}

max-boolean-question : C ℕ → ℕ
max-boolean-question (D.η n)   = 0
max-boolean-question (D.β φ n) = max n (max n₁ n₂)
 where
  n₁ : ℕ
  n₁ = max-boolean-question (φ ₀)

  n₂ : ℕ
  n₂ = max-boolean-question (φ ₁)

max-boolean-question⋆ : D⋆ ℕ ℕ ℕ ℕ → ℕ
max-boolean-question⋆ d = d (λ _ → 0) (λ g x → max x (max (g 0) (g 1)))

max-boolean-questionᵀ : {Γ : Cxt} → Γ ⊢ (⌜B⌝ ι ι) ⇒ ι
max-boolean-questionᵀ =
 ƛ
  (ν₀
   · (ƛ Zero)
   · ƛ (ƛ (maxᵀ · ν₀ · (maxᵀ · (ν₁ · numeral 0)
                             · (ν₁ · numeral 1)))))

\end{code}

We now prove two lemmas capturing the agreement of `max-boolean-question`,
`max-boolean-question⋆`, and `max-boolean-questionᵀ`.

\begin{code}

max-boolean-question⋆-agreement : (d : B ℕ)
                                → max-boolean-question (prune d)
                                  ＝ max-boolean-question⋆ (church-encode d)
max-boolean-question⋆-agreement (D.η n)   = refl
max-boolean-question⋆-agreement (D.β φ n) = †
 where
  encode = church-encode

  IH₀ : max-boolean-question (prune (φ 0))
        ＝ max-boolean-question⋆ (encode (φ 0))
  IH₀ = max-boolean-question⋆-agreement (φ 0)

  IH₁ : max-boolean-question (prune (φ 1))
        ＝ max-boolean-question⋆ (encode (φ 1))
  IH₁ = max-boolean-question⋆-agreement (φ 1)

  n₀  = max-boolean-question (prune (φ 0))
  n₁  = max-boolean-question (prune (φ 1))
  n₀⋆ = max-boolean-question⋆ (encode (φ 0))
  n₁⋆ = max-boolean-question⋆ (encode (φ 1))

  Ⅰ = ap (λ - → max n (max - (max-boolean-question (prune (φ 1)))))          IH₀
  Ⅱ = ap (λ - → max n (max (max-boolean-question⋆ (church-encode (φ 0))) -)) IH₁

  † : max-boolean-question (prune (D.β φ n))
      ＝ max-boolean-question⋆ (encode (D.β φ n))
  † =
   max-boolean-question (D.β ((λ j → prune (φ (embedding-𝟚-ℕ j)))) n) ＝⟨ refl ⟩
   max n (max n₀  n₁)                                                 ＝⟨ Ⅰ    ⟩
   max n (max n₀⋆ n₁)                                                 ＝⟨ Ⅱ    ⟩
   max n (max n₀⋆ n₁⋆)                                                ＝⟨ refl ⟩
   max-boolean-question⋆ (encode (D.β φ n))                           ∎

max-boolean-questionᵀ-agreement : (d : 〈〉 ⊢ ⌜D⋆⌝ ι ι ι ι)
                                → ⟦ max-boolean-questionᵀ · d ⟧₀
                                  ＝ max-boolean-question⋆ ⟦ d ⟧₀
max-boolean-questionᵀ-agreement d =
 ⟦ max-boolean-questionᵀ · d ⟧₀                                  ＝⟨ refl  ⟩
 ⟦ d ⟧₀ (λ _ → 0) (λ g x → ⟦ maxᵀ ⟧₀ x (⟦ maxᵀ ⟧₀ (g 0) (g 1)))  ＝⟨ Ⅰ     ⟩
 ⟦ d ⟧₀ (λ _ → 0) (λ g x → max x (⟦ maxᵀ ⟧₀ (g 0) (g 1)))        ＝⟨ Ⅱ     ⟩
 ⟦ d ⟧₀ (λ _ → 0) (λ g x → max x (max (g 0) (g 1)))              ＝⟨ refl  ⟩
 max-boolean-question⋆ ⟦ d ⟧₀                                    ∎
  where
   † : (g : ℕ → ℕ) (n : ℕ)
     → ⟦ maxᵀ ⟧₀ n (⟦ maxᵀ ⟧₀ (g 0) (g 1)) ＝ max n (⟦ maxᵀ ⟧₀ (g 0) (g 1))
   † g n = maxᵀ-correct n (⟦ maxᵀ ⟧₀ (g 0) (g 1))

   ‡ : (g : ℕ → ℕ) (n : ℕ)
     → max n (⟦ maxᵀ ⟧₀ (g 0) (g 1)) ＝ max n (max (g 0) (g 1))
   ‡ g n = ap (max n) (maxᵀ-correct (g 0) (g 1))

   Ⅰ = ap (⟦ d ⟧₀ (λ _ → 0)) (dfunext fe λ g → dfunext fe λ n → † g n)
   Ⅱ = ap (⟦ d ⟧₀ (λ _ → 0)) (dfunext fe λ g → dfunext fe λ n → ‡ g n)

\end{code}

The following is an analogue of `main-lemma` from the `InternalModCont` module.

\begin{code}

main-lemma : (t : 〈〉 ⊢ baire ⇒ ι)
           → ⟦ max-boolean-questionᵀ · ⌜dialogue-tree⌝ t ⟧₀
             ＝ max-boolean-question (prune (dialogue-tree t))
main-lemma t =
 ⟦ max-boolean-questionᵀ · ⌜dialogue-tree⌝ t ⟧₀             ＝⟨ refl ⟩
 ⟦ max-boolean-questionᵀ ⟧₀ ⟦ ⌜dialogue-tree⌝ t ⟧₀          ＝⟨ Ⅰ    ⟩
 max-boolean-question⋆ ⟦ ⌜dialogue-tree⌝ t ⟧₀               ＝⟨ Ⅱ    ⟩
 max-boolean-question⋆ (church-encode (dialogue-tree t ))   ＝⟨ Ⅲ    ⟩
 max-boolean-question (prune (dialogue-tree t))             ∎
  where
   † : Rnorm (B⟦ t ⟧₀ generic) (⌜ t ⌝ · ⌜generic⌝)
   † = Rnorm-lemma₀ t generic ⌜generic⌝ Rnorm-generic

   γ : (f : ℕ → ℕ) (g : ℕ → ℕ)
     → ({m n : ℕ} → m ＝ n → f m ＝ g n)
     → {m n : ℕ} → m ＝ n → max m (max (f 0) (f 1)) ＝ max n (max (g 0) (g 1))
   γ f g φ {m} {n} p = max m (max (f 0) (f 1)) ＝⟨ Ⅰ ⟩
                         max n (max (f 0) (f 1)) ＝⟨ Ⅱ ⟩
                         max n (max (g 0) (f 1)) ＝⟨ Ⅲ ⟩
                         max n (max (g 0) (g 1)) ∎
                          where
                           Ⅰ = ap (λ - → max - (max (f 0) (f 1))) p
                           Ⅱ = ap (λ - → max n (max - (f 1))) (φ refl)
                           Ⅲ = ap (λ - → max n (max (g 0) -)) (φ refl)

   Ⅰ = max-boolean-questionᵀ-agreement (⌜dialogue-tree⌝ t)
   Ⅱ = † (λ _ → refl) (λ {f} {g} → γ f g)
   Ⅲ = max-boolean-question⋆-agreement (dialogue-tree t) ⁻¹

\end{code}

We know by `dialogue-UC` that the function encoded by a dialogue tree is
uniformly continuous. We denote by `mod-of` the operation of taking the modulus
of uniform continuity of such a computation encoded by a dialogue tree. It
assumes that the dialogue tree in consideration is binary, and accordingly,
first prunes the tree.

\begin{code}

mod-of : B ℕ → BT ℕ
mod-of d = pr₁ (dialogue-UC (prune d))

\end{code}

We also prove a lemma showing that `max-boolean-question ∘ prune` is the same
thing as `maximumᵤ ∘ mod-of`.

\begin{code}

max-boolean-question-is-maximum-mod-of : (d : B ℕ)
                                        → max-boolean-question (prune d)
                                          ＝ maximumᵤ (mod-of d)
max-boolean-question-is-maximum-mod-of (D.η n)   = refl
max-boolean-question-is-maximum-mod-of (D.β φ n) =
 max-boolean-question (prune (D.β φ n))                            ＝⟨ refl ⟩
 max-boolean-question (D.β (λ j → prune (φ (embedding-𝟚-ℕ j))) n)  ＝⟨ refl ⟩
 max n (max n₀ n₁)                                                 ＝⟨ Ⅰ    ⟩
 max n (max (maximumᵤ (mod-of (φ 0))) n₁)                          ＝⟨ Ⅱ    ⟩
 max n (max (maximumᵤ (mod-of (φ 0))) (maximumᵤ (mod-of (φ 1))))   ＝⟨ refl ⟩
 maximumᵤ (mod-of (D.β φ n))                                       ∎
  where
   Ⅰ   = ap
          (λ - → max n (max - (max-boolean-question (prune (φ 1)))))
          (max-boolean-question-is-maximum-mod-of (φ 0))
   Ⅱ   = ap
          (max n ∘ max (maximumᵤ (mod-of (φ 0))))
          (max-boolean-question-is-maximum-mod-of (φ 1))

   n₀  = max-boolean-question (prune (φ 0))
   n₁  = max-boolean-question (prune (φ 1))

\end{code}

We now proceed to define the analogue of `modulus` from `InternalModCont`,
following the same notational conventions.

\begin{code}

modulusᵤ : C ℕ → ℕ
modulusᵤ = succ ∘ max-boolean-question

\end{code}

The internalized version of `modulusᵤ` is denoted by `modulusᵤᵀ`.

\begin{code}

modulusᵤᵀ : {Γ : Cxt} →  Γ ⊢ baire ⇒ ι → B-context【 Γ 】 ι ⊢ ι
modulusᵤᵀ t = Succ' · (max-boolean-questionᵀ · ⌜dialogue-tree⌝ t)

\end{code}

We also need to write down the completely obvious fact that a function
`f : Baire → ℕ` agrees with the restriction of `f` to Cantor, when considering
Boolean points.

\begin{code}

agreement-with-restriction : (f : Baire → ℕ) (α : Baire)
                           → (bv : is-boolean-point α)
                           → f α ＝ C-restriction f (to-cantor (α , bv))
agreement-with-restriction f α bv =
 f α                                   ＝⟨ refl ⟩
 f′ (α , bv)                           ＝⟨ †    ⟩
 f′ (to-cantor₀ (to-cantor (α , bv)))  ＝⟨ refl ⟩
 f₀ (to-cantor (α , bv))               ∎
  where
   f₀ : Cantor → ℕ
   f₀ = C-restriction f

   f′ : Cantor₀ → ℕ
   f′ = f ∘ pr₁

   † = ap f′ (to-cantor₀-cancels-to-cantor (α , bv) ⁻¹)

\end{code}

Finally, we state and prove our main result:

  given any Boolean `t : baire ⇒ ι`, and given any two Boolean points `αᵀ, βᵀ :
  baire`, if `⟦ αᵀ ⟧` is equal to `⟦ βᵀ ⟧` up to `modulusᵤᵀ t`, then `⟦ t · αᵀ
  ⟧` is equal to `⟦ t · βᵀ ⟧`.

\begin{code}

internal-uni-mod-correct : (t : 〈〉 ⊢ baire ⇒ ι) (αᵀ βᵀ : 〈〉 ⊢ baire)
                         → is-boolean-pointᵀ αᵀ
                         → is-boolean-pointᵀ βᵀ
                         → ⟦ αᵀ ⟧₀ ＝⦅ ⟦ modulusᵤᵀ t ⟧₀ ⦆ ⟦ βᵀ ⟧₀
                         → ⟦ t · αᵀ ⟧₀ ＝ ⟦ t · βᵀ ⟧₀
internal-uni-mod-correct t αᵀ βᵀ ψ₁ ψ₂ φ =
 f α ＝⟨ Ⅰ ⟩ f₀ (to-cantor α₀) ＝⟨ Ⅱ ⟩ f₀ (to-cantor β₀) ＝⟨ Ⅲ ⟩ f β ∎
  where
   f : Baire → ℕ
   f = ⟦ t ⟧₀

   α : Baire
   α = ⟦ αᵀ ⟧₀

   β : Baire
   β = ⟦ βᵀ ⟧₀

   α₀ : Cantor₀
   α₀ = α , boolean-valuedᵀ-lemma αᵀ ψ₁

   β₀ : Cantor₀
   β₀ = β , boolean-valuedᵀ-lemma βᵀ ψ₂

   f₀ : Cantor → ℕ
   f₀ = C-restriction f

   ε : eloquent f
   ε = eloquence-theorem ⟦ t ⟧₀ (t , refl)

   ε₀ : eloquent f₀
   ε₀ = restriction-is-eloquent f ε

   c : is-uniformly-continuous f₀
   c = eloquent-functions-are-UC f₀ ε₀

   bt : BT ℕ
   bt = mod-of (dialogue-tree t)

   c₀ : is-uniformly-continuous₀ f₀
   c₀ = uni-continuity-implies-uni-continuity₀ f₀ c

   mᵘ₀ : ℕ
   mᵘ₀ = succ (maximumᵤ bt)

   ξ : ⟦ max-boolean-questionᵀ · ⌜dialogue-tree⌝ t ⟧₀ ＝ maximumᵤ bt
   ξ = ⟦ max-boolean-questionᵀ · ⌜dialogue-tree⌝ t ⟧₀   ＝⟨ Ⅰ ⟩
       max-boolean-question (prune (dialogue-tree t))   ＝⟨ Ⅱ ⟩
       maximumᵤ bt                                      ∎
        where
         Ⅰ = main-lemma t
         Ⅱ = max-boolean-question-is-maximum-mod-of (dialogue-tree t)

   q : ⟦ modulusᵤᵀ t ⟧₀ ＝ succ (maximumᵤ bt)
   q = ap succ ξ

   ψ : α ＝⦅ succ (maximumᵤ bt) ⦆ β
   ψ = transport (λ - → α ＝⦅ - ⦆ β) q φ

   ρ : α ＝⦅ succ (maximum (sequentialize bt)) ⦆ β
   ρ = transport
        (λ - → α ＝⦅ - ⦆ β)
        (ap succ (maximumᵤ′-equivalent-to-maximumᵤ bt))
        ψ

   η : α ＝⟪ sequentialize bt ⟫ β
   η = ＝⦅⦆-implies-＝⟪⟫ α β (sequentialize bt) ρ

   ζ : α ＝⟪ sequentialize bt ⟫₀ β
   ζ = ＝⟪⟫-implies-＝⟪⟫₀ α β (sequentialize bt) η

   δ : α ＝⟦ bt ⟧ β
   δ = ＝⟪⟫₀-implies-＝⟦⟧ α β bt ζ

   γ : to-cantor α₀ ＝⟦ bt ⟧ to-cantor β₀
   γ = to-cantor-＝⟦⟧
        (boolean-valuedᵀ-lemma αᵀ ψ₁)
        (boolean-valuedᵀ-lemma βᵀ ψ₂)
        bt
        δ

   Ⅱ = pr₂ c (to-cantor α₀) (to-cantor β₀) γ

   Ⅰ = agreement-with-restriction f α (boolean-valuedᵀ-lemma αᵀ ψ₁)
   Ⅲ = agreement-with-restriction f β (boolean-valuedᵀ-lemma βᵀ ψ₂) ⁻¹

\end{code}
