Chuangjie Xu, 2013

This corresponds to section 4.1 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

The axiom of uniform continuity is not provable in system T or
HAω. But it can be realized in our model by the following Fan
functional:

       fan : Map ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace

which continuously computes the moduli of uniform continuity.

\begin{code}


module Fan where

open import MiniLibrary
open import Sequence
open import Inequality
open import UniformContinuity
open import Space
open import Space-exponential
open import Space-discrete
open import Space-cantor
open import not-not
open import not-not-funext

\end{code}

To show the continuity of the fan functional, we need the
following auxiliaries.

\begin{code}


_×2 : ℕ → ℕ
_×2         = 
_×2 (succ n) = succ (succ (n ×2))

Lemma[n≤2n] : ∀(n : ℕ) → n ≤ (n ×2)
Lemma[n≤2n]         = ≤-zero
Lemma[n≤2n] (succ n) = Lemma[a≤b≤c→a≤c] (≤-succ (Lemma[n≤2n] n))
                                        (Lemma[n≤n+1] (succ (n ×2)))

Lemma[n<m→2n<2m] : ∀(n m : ℕ) → n < m → (n ×2) < (m ×2)
Lemma[n<m→2n<2m]                 ()
Lemma[n<m→2n<2m]         (succ m) _          = ≤-succ ≤-zero
Lemma[n<m→2n<2m] (succ n)         ()
Lemma[n<m→2n<2m] (succ n) (succ m) (≤-succ r) = ≤-succ (≤-succ (Lemma[n<m→2n<2m] n m r))


_×2+1 : ℕ → ℕ
_×2+1         = 
_×2+1 (succ n) = succ (succ (n ×2+1))

Lemma[n≤2n+1] : ∀(n : ℕ) → n ≤ (n ×2+1)
Lemma[n≤2n+1]         = ≤-zero
Lemma[n≤2n+1] (succ n) = Lemma[a≤b≤c→a≤c] (≤-succ (Lemma[n≤2n+1] n))
                                          (Lemma[n≤n+1] (succ (n ×2+1)))

Lemma[n<m→2n+1<2m+1] : ∀(n m : ℕ) → n < m → (n ×2+1) < (m ×2+1)
Lemma[n<m→2n+1<2m+1]                 ()
Lemma[n<m→2n+1<2m+1]         (succ m) _          = ≤-succ (≤-succ ≤-zero)
Lemma[n<m→2n+1<2m+1] (succ n)         ()
Lemma[n<m→2n+1<2m+1] (succ n) (succ m) (≤-succ r) = ≤-succ (≤-succ (Lemma[n<m→2n+1<2m+1] n m r))


\end{code}

Here is the fan functional, which calculates smallest moduli, using
the moduli obtained by Yoneda Lemma.

\begin{code}


fan : Map ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) ℕSpace
fan = f , cts
 where
  f : U((ℕSpace ⇒ ₂Space) ⇒ ℕSpace) → ℕ
  f φ = ∃-witness (∃-elim (Lemma[Yoneda] {ℕSpace} φ))
  cts : continuous {(ℕSpace ⇒ ₂Space) ⇒ ℕSpace} {ℕSpace} f
  cts p pr = Lemma[LM-ℕ-least-modulus] (f ∘ p) n prf
   where
    t₀ : ₂ℕ → ₂ℕ
    t₀ α = α ∘ _×2
    uct₀ : t₀ ∈ C
    uct₀ m = Lemma[LM-₂ℕ-least-modulus] t₀ (m ×2) prf₁
     where
      prf₀ : ∀(α β : ₂ℕ) → α ≣[ m ×2 ] β → ∀(i : ℕ) → i < m → t₀ α i ≡ t₀ β i
      prf₀ α β aw i i<m = Lemma[≣[]-<] aw (i ×2) (Lemma[n<m→2n<2m] i m i<m)
      prf₁ : ∀(α β : ₂ℕ) → α ≣[ m ×2 ] β → t₀ α ≣[ m ] t₀ β
      prf₁ α β aw = Lemma[<-≣[]] (prf₀ α β aw)

    t₁ : ₂ℕ → ₂ℕ
    t₁ α = α ∘ _×2+1
    uct₁ : t₁ ∈ C
    uct₁ m = Lemma[LM-₂ℕ-least-modulus] t₁ (m ×2+1) prf₁
     where
      prf₀ : ∀(α β : ₂ℕ) → α ≣[ m ×2+1 ] β → ∀(i : ℕ) → i < m → t₁ α i ≡ t₁ β i
      prf₀ α β aw i i<m = Lemma[≣[]-<] aw (i ×2+1) (Lemma[n<m→2n+1<2m+1] i m i<m)
      prf₁ : ∀(α β : ₂ℕ) → α ≣[ m ×2+1 ] β → t₁ α ≣[ m ] t₁ β
      prf₁ α β aw = Lemma[<-≣[]] (prf₀ α β aw)

    t₁' : ₂ℕ → U(ℕSpace ⇒ ₂Space)
    t₁' = ∃-witness (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] t₁ uct₁)
    pr₁ : t₁' ∈ Probe (ℕSpace ⇒ ₂Space)
    pr₁ = ∃-elim (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] t₁ uct₁)

    merge : ₂ℕ → ₂ℕ → ₂ℕ
    merge α β                = α 
    merge α β                = β 
    merge α β (succ (succ i)) = merge (α ∘ succ) (β ∘ succ) i

    lemma' : ∀(α β γ : ₂ℕ) → ∀(k : ℕ) → α ≣[ k ] β → ∀(i : ℕ) → i < (k ×2) → merge α γ i ≡ merge β γ i
    lemma' α β γ         aw i ()
    lemma' α β γ (succ k) aw  r = Lemma[≣[]-<] aw zero (≤-succ ≤-zero)
    lemma' α β γ (succ k) aw  r = refl
    lemma' α β γ (succ k) aw (succ (succ i)) (≤-succ (≤-succ r)) =
          lemma' (α ∘ succ) (β ∘ succ) (γ ∘ succ) k (Lemma[≣[]-succ] aw) i r

    lemma : ∀(α β γ : ₂ℕ) → ∀(k : ℕ) → α ≣[ k ] β → merge α γ ≣[ k ×2 ] merge β γ
    lemma α β γ k ek = Lemma[<-≣[]] (lemma' α β γ k ek)

    lemma₀ : ∀(α β : ₂ℕ) → [ t₀ (merge α β) ≡ α ]
    lemma₀ α β = funext¹ (le α β)
                 ------
     where
      le : ∀(α β : ₂ℕ) → ∀(i : ℕ) → t₀ (merge α β) i ≡ α i
      le α β         = refl
      le α β (succ i) = le (α ∘ succ) (β ∘ succ) i

    lemma₁ : ∀(α β : ₂ℕ) → ∀(i : ℕ) → t₁ (merge α β) i ≡ β i
    lemma₁ α β         = refl
    lemma₁ α β (succ i) = lemma₁ (α ∘ succ) (β ∘ succ) i

    lemma₁' : ∀(α : ₂ℕ) → ∀(φ : Map ℕSpace ₂Space) →
               [ t₁' (merge α (π₀  φ)) ≡ φ ]
    lemma₁' α (γ , ctsγ) = Lemma[Map-₂] ℕSpace (β , ctsβ) (γ , ctsγ) claim
     where
      β : ₂ℕ
      β = π₀ (t₁' (merge α γ))
      ctsβ : continuous {ℕSpace} {₂Space} β
      ctsβ = π₁ (t₁' (merge α γ))
      claim : ∀(i : ℕ) → β i ≡ γ i
      claim = lemma₁ α γ

    q : ₂ℕ → ℕ
    q α = (π₀ ∘ p)(t₀ α)(t₁' α)
    ucq : locally-constant q
    ucq = pr t₁' pr₁ t₀ uct₀

    n : ℕ
    n = ∃-witness ucq

    claim : ∀(α β : ₂ℕ) → α ≣[ n ] β → [ p α ≡ p β ]
    claim α β en = Lemma[Map-ℕ] (ℕSpace ⇒ ₂Space) (pα , ctsα) (pβ , ctsβ) sclaim
     where
      pα : Map ℕSpace ₂Space → ℕ
      pα = π₀ (p α)
      ctsα : continuous {ℕSpace ⇒ ₂Space} {ℕSpace} pα
      ctsα = π₁ (p α)
      pβ : Map ℕSpace ₂Space → ℕ
      pβ = π₀ (p β)
      ctsβ : continuous {ℕSpace ⇒ ₂Space} {ℕSpace} pβ
      ctsβ = π₁ (p β)
      sclaim : ∀(γ : Map ℕSpace ₂Space) → pα γ ≡ pβ γ
      sclaim (γ , ctsγ) = decidable-structure (ℕ-discrete (pα (γ , ctsγ)) (pβ (γ , ctsγ))) ssclaim₄
       where
        eγ : merge α γ ≣[ n ] merge β γ
        eγ = Lemma[≣[]-≤] (lemma α β γ n en) (Lemma[n≤2n] n)
        ssclaim₀ : [ (π₀ ∘ p)(t₀ (merge α γ))(t₁' (merge α γ)) ≡ (π₀ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ)) ]
        ssclaim₀ = hide (∧-elim₀ (∃-elim ucq) (merge α γ) (merge β γ) eγ)
        ssclaim₁ : [ (π₀ ∘ p)(α)(t₁' (merge α γ)) ≡ (π₀ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ)) ]
        ssclaim₁ = [transport] {₂ℕ} {λ x → (π₀ ∘ p)(x)(t₁' (merge α γ)) ≡ (π₀ ∘ p)(t₀ (merge β γ))(t₁' (merge β γ))}
                           (lemma₀ α γ) ssclaim₀
        ssclaim₂ : [ π₀ (p α) (t₁' (merge α γ)) ≡ π₀ (p β) (t₁' (merge β γ)) ]
        ssclaim₂ = [transport] {₂ℕ} {λ x → (π₀ ∘ p)(α)(t₁' (merge α γ)) ≡ (π₀ ∘ p)(x)(t₁' (merge β γ))}
                           (lemma₀ β γ) ssclaim₁
        ssclaim₃ : [ π₀ (p α) (γ , ctsγ) ≡ π₀ (p β) (t₁' (merge β γ)) ]
        ssclaim₃ = [transport] {Map ℕSpace ₂Space} {λ x → π₀ (p α) (x) ≡ π₀ (p β) (t₁' (merge β γ))}
                           (lemma₁' α (γ , ctsγ)) ssclaim₂
        ssclaim₄ : [ π₀ (p α) (γ , ctsγ) ≡ π₀ (p β) (γ , ctsγ) ]
        ssclaim₄ = [transport] {Map ℕSpace ₂Space} {λ x → π₀ (p α) (γ , ctsγ) ≡ π₀ (p β) (x)}
                           (lemma₁' β (γ , ctsγ)) ssclaim₃

    prf : ∀(α β : ₂ℕ) → α ≣[ n ] β → (f ∘ p) α ≡ (f ∘ p) β
    prf α β en = Lemma[[≡]→≡]-ℕ ([ap] f (claim α β en))


fan-behaviour : ∀(f : U ((ℕSpace ⇒ ₂Space) ⇒ ℕSpace)) →
                ∀(α β : U (ℕSpace ⇒ ₂Space)) → π₀ α ≣[ π₀ fan f ] π₀ β → π₀ f α ≡ π₀ f β
fan-behaviour f α β r = Lemma[[≡]→≡]-ℕ [goal]
 where
  f' : ₂ℕ → ℕ
  f' = ∃-witness (Lemma[Yoneda] {ℕSpace} f)
  claim : [ f' (π₀ α) ≡ f' (π₀ β) ]
  claim = hide (∧-elim₀(∃-elim (∃-elim (Lemma[Yoneda] {ℕSpace} f))) (π₀ α) (π₀ β) r)
  eqα : [ π₀ f α ≡ f' (π₀ α) ]
  eqα = [ap] (π₀ f) (Lemma[ID-[≡]] α)
  eqβ : [ π₀ f β ≡ f' (π₀ β) ]
  eqβ = [ap] (π₀ f) (Lemma[ID-[≡]] β)
  [goal] : [ π₀ f α ≡ π₀ f β ]
  [goal] = [trans] ([trans] eqα claim) ([sym] eqβ)

\end{code}